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 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/proofview.ml')

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