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

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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