aboutsummaryrefslogtreecommitdiff
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 af9fb662bf..665b0c9e59 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -57,9 +57,6 @@ module V82 : sig
(* Principal part of the progress tactical *)
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
- (* Principal part of tclNOTSAMEGOAL *)
- val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
-
(* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map