From bf840bafc19deba67e5270dfd31b8b6662b73132 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 26 Feb 2019 23:41:38 +0100
Subject: Fix #9652: rewrite fails to detect lack of progress

---
 engine/proofview.ml               |  6 +++---
 engine/proofview.mli              |  6 +++++-
 proofs/goal.ml                    | 11 +----------
 proofs/goal.mli                   |  3 ---
 tactics/equality.ml               |  2 +-
 test-suite/bugs/closed/bug_9652.v | 19 +++++++++++++++++++
 6 files changed, 29 insertions(+), 18 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_9652.v

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2d693e0259..316f02bc37 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -899,8 +899,8 @@ module Progress = struct
 
   (** Equality function on goals *)
   let goal_equal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 (drop_state gl1) in
-    let evi2 = Evd.find evars2 (drop_state gl2) in
+    let evi1 = Evd.find evars1 gl1 in
+    let evi2 = Evd.find evars2 gl2 in
     eq_evar_info evars1 evars2 evi1 evi2
 
 end
@@ -918,7 +918,7 @@ let tclPROGRESS t =
   let test =
     quick_test ||
     Util.List.for_all2eq begin fun i f ->
-      Progress.goal_equal initial.solution i final.solution f
+      Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
     end initial.comb final.comb
   in
   if not test then
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 680a93f0cc..c772525c86 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -395,10 +395,14 @@ val give_up : unit tactic
 (** {7 Control primitives} *)
 
 (** [tclPROGRESS t] checks the state of the proof after [t]. It it is
-    identical to the state before, then [tclePROGRESS t] fails, otherwise
+    identical to the state before, then [tclPROGRESS t] fails, otherwise
     it succeeds like [t]. *)
 val tclPROGRESS : 'a tactic -> 'a tactic
 
+module Progress : sig
+  val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+end
+
 (** Checks for interrupts *)
 val tclCHECKINTERRUPT : unit tactic
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index e5688fe730..94707accab 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -89,18 +89,9 @@ module V82 = struct
     | None -> sigma
     | Some id -> Evd.rename evk' id sigma
 
-  (* Parts of the progress tactical *)
-  let same_goal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 gl1 in
-    let evi2 = Evd.find evars2 gl2 in
-    let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in
-    let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in
-    Constr.equal c1 c2 &&
-    Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
-
   let weak_progress glss gls =
     match glss.Evd.it with
-    | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
+    | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
     | _ -> true
 
   let progress glss gls =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index af9fb662bf..665b0c9e59 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -57,9 +57,6 @@ module V82 : sig
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
 
- (* Principal part of tclNOTSAMEGOAL *)
-  val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
-
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 88ce9868af..412fbbfd1b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -257,7 +257,7 @@ let tclNOTSAMEGOAL tac =
     Proofview.Goal.goals >>= fun gls ->
     let check accu gl' =
       gl' >>= fun gl' ->
-      let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+      let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in
       Proofview.tclUNIT accu
     in
     Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
diff --git a/test-suite/bugs/closed/bug_9652.v b/test-suite/bugs/closed/bug_9652.v
new file mode 100644
index 0000000000..21ce1bea61
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9652.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+Require Import Coq.ZArith.BinInt.
+Class word_interface (width : Z) : Type := Build_word
+  { rep : Type;
+    unsigned : rep -> Z;
+    of_Z : Z -> rep;
+    sub : rep -> rep -> rep }.
+Coercion rep : word_interface >-> Sortclass.
+Axiom word : word_interface 64. Local Existing Instance word.
+Goal
+  forall (x : list word) (x1 x2 : word),
+  (unsigned (sub x2 x1) / 2 ^ 4 * 2 ^ 3 <
+   unsigned (of_Z 8) * Z.of_nat (Datatypes.length x))%Z.
+Proof.
+  intros.
+  assert (unsigned (sub x2 x1) = unsigned (sub x2 x1)) by exact eq_refl.
+  Fail progress rewrite H.
+  Fail rewrite H.
+Abort.
-- 
cgit v1.2.3