Fix w.r.t. EasyCrypt c0e1455

formosa-crypto · Apr 13, 2024 · 7222f3f · 7222f3f
1 parent 643103e
commit 7222f3f
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/proof/correctness/avx2/NTT_AVX_Fq.ec b/proof/correctness/avx2/NTT_AVX_Fq.ec
@@ -2063,7 +2063,8 @@ seq 12 1: (CS2P [r0i;r1i;r2i;r3i;r4i;r5i;r6i;r7i;r0t;r1t;r2t;r3t;r4t;r5t;r6t;r7t
  by inline *; auto => /> *; rewrite !P2C_i => />.
 (* level 5 *)
 seq 21 1: (rp{1} = rp5{2}).
-  by inline *; auto => />*; rewrite !P2C_i => />; rewrite P2CS !PUC_i => />. 
+  inline *; auto => /> &1 *; rewrite !P2C_i => />.
+  by rewrite [rp{1}]P2CS !PUC_i => />. 
 by inline *; auto => />*.
 qed.