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 dc9863156..b8c979ad7 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -64,9 +64,6 @@ module V82 : sig
(* Principal part of tclNOTSAMEGOAL *)
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
- (* Used for congruence closure *)
- val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
-
(* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map