From 21ee9a82807176acecf917e2a1e6074bed1c88ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 18:16:27 +0100
Subject: Removing the tclWEAK_PROGRESS tactical.

The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
---
 proofs/goal.mli    | 3 ---
 proofs/refiner.ml  | 7 -------
 proofs/refiner.mli | 1 -
 3 files changed, 11 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal.mli b/proofs/goal.mli
index a2fa34c05e..ee2e736120 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -59,9 +59,6 @@ module V82 : sig
      second goal *)
   val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
-  (* Principal part of the weak-progress tactical *)
-  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-   
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
     
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index d086f0bbca..bc12b3ba71 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -160,13 +160,6 @@ let rec tclTHENLIST = function
 let tclMAP tacfun l =
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
-the goal unchanged *)
-let tclWEAK_PROGRESS tac ptree =
-  let rslt = tac ptree in
-  if Goal.V82.weak_progress rslt ptree then rslt
-  else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.")
-
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
 let tclPROGRESS tac ptree =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index de6502dc36..e179589df2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,7 +119,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
 
-- 
cgit v1.2.3