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.

6 files changed, 1 insertions, 15 deletions

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
@@ -162,13 +162,6 @@ let tclMAP tacfun l =
 
 (* 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 =
   let rslt = tac ptree in
   if Goal.V82.progress rslt ptree then rslt
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
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index df222eed80..d70275dee5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -462,8 +462,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
-         let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
-         Proofview.V82.tactic (tclWEAK_PROGRESS tac)
+         Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
       let tac = run_hint t tac in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 97922a4fa5..5c97f27bab 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -51,7 +51,6 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
 let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
 let tclTHENTRY       = Refiner.tclTHENTRY
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 33933924ab..01b9e5e936 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,7 +44,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic