Work around bug #5453

This is https://coq.inria.fr/bugs/show_bug.cgi?id=5453, Bogus error message "Error: foo depends on the variable x which is not declared in the context." (issue with subst and proof using)
mit-plv · Apr 4, 2017 · 0529211 · 0529211
1 parent 331fe3f
commit 0529211
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v
@@ -102,7 +102,7 @@ Section barrett.
     Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q.
       Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div.
       assert (a mod n < n) by auto with zarith lia.
-      subst r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m.
+      unfold r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m.
       autorewrite with push_Zmul zsimplify zstrip_div.
       break_match; auto with lia.
     Qed.

diff --git a/src/ModularArithmetic/BarrettReduction/ZGeneralized.v b/src/ModularArithmetic/BarrettReduction/ZGeneralized.v
@@ -119,7 +119,7 @@ Section barrett.
     Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg q.
       Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div.
       assert (a mod n < n) by auto with zarith lia.
-      subst r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m.
+      unfold r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m.
       autorewrite with push_Zmul zsimplify zstrip_div.
       break_match; auto with lia.
     Qed.