hmac_tag should not be [data]

cryspen · Mar 25, 2024 · 2a612f4 · 2a612f4
1 parent 80be87f
commit 2a612f4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proofs/proverif/extraction/lib.pvl b/proofs/proverif/extraction/lib.pvl
@@ -2528,7 +2528,7 @@ fun bertie__tls13crypto__hmac_tag(
       bertie__tls13utils__t_Bytes,
       bertie__tls13utils__t_Bytes
     )
-    : bertie__tls13utils__t_Bytes [data].
+    : bertie__tls13utils__t_Bytes.
 
 
 letfun bertie__tls13utils__impl__Bytes__as_raw(