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.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'engine/proofview.mli')

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