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

---
 proofs/goal.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'proofs/goal.ml')

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 =
-- 
cgit v1.2.3