Merge pull request #33 from ppedrot/specialize-evar-clause

Adapt w.r.t. coq/coq#17322.
mit-plv · Mar 2, 2023 · f193b6e · f193b6e
2 parents e7204f3 + 2e43524
commit f193b6e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/riscv/Platform/MinimalNoMul.v b/src/riscv/Platform/MinimalNoMul.v
@@ -208,8 +208,8 @@ Section Riscv.
       unfold map.getmany_of_tuple, Memory.footprint in IHn.
       specialize IHn with (m := m) (r := (word.add r (word.of_Z 1))).
       rewrite E1 in IHn.
-      specialize IHn with (1 := eq_refl).
       eapply IHn.
+      + reflexivity.
       + instantiate (1 := someSet). clear -H0.
         unfold isXAddr4 in *. fwd. eauto 10 using removeXAddr_bw.
       + unfold Memory.load_bytes in *.