Merge branch 'main' into wysiwys/docker-c-extraction

cryspen · Feb 10, 2025 · 84f163a · 84f163a
2 parents 976720d + 02e7788
commit 84f163a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst
@@ -62,8 +62,8 @@ let t_VerificationError_cast_to_repr (x: t_VerificationError) =
   match x <: t_VerificationError with
   | VerificationError_MalformedHintError  -> mk_isize 0
   | VerificationError_SignerResponseExceedsBoundError  -> mk_isize 1
-  | VerificationError_CommitmentHashesDontMatchError  -> mk_isize 3
-  | VerificationError_VerificationContextTooLongError  -> mk_isize 6
+  | VerificationError_CommitmentHashesDontMatchError  -> mk_isize 2
+  | VerificationError_VerificationContextTooLongError  -> mk_isize 3
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume