aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r--proofs/goal.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a2fa34c05..ee2e73612 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