diff options
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index dc986315..a033d6da 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 @@ -74,3 +71,5 @@ module V82 : sig val abstract_type : Evd.evar_map -> goal -> EConstr.types end + +module Set : sig include Set.S with type elt = goal end |