diff options
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r-- | proofs/goal.mli | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index 7c8fdef29..7a14848b5 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -34,10 +34,6 @@ module V82 : sig (* Old style env primitive *) val env : Evd.evar_map -> goal -> Environ.env - (* same as [env], but ensures that existential variables are - normalised *) - val nf_env : Evd.evar_map -> goal -> Environ.env - (* Old style hyps primitive *) val hyps : Evd.evar_map -> goal -> Environ.named_context_val @@ -48,16 +44,9 @@ module V82 : sig (* Access to ".evar_concl" *) val concl : Evd.evar_map -> goal -> Term.constr - (* same as [concl] but ensures that existential variables are - normalised. *) - val nf_concl : Evd.evar_map -> goal -> Term.constr - (* Access to ".evar_extra" *) val extra : Evd.evar_map -> goal -> Evd.Store.t - (* Old style filtered_context primitive *) - val filtered_context : Evd.evar_map -> goal -> Context.named_context - (* Old style mk_goal primitive, returns a new goal with corresponding hypotheses and conclusion, together with a term which is precisely the evar corresponding to the goal, and an updated evar_map. *) @@ -67,15 +56,6 @@ module V82 : sig Evd.Store.t -> goal * Term.constr * Evd.evar_map - (* Creates a dummy [goal sigma] for use in auto *) - val dummy_goal : goal Evd.sigma - - (* Makes a goal out of an evar *) - (* spiwack: used by [Proofview.init], not entirely clean probably, but it is - the only way I could think of to preserve compatibility with previous Coq - stuff. *) - val build : Evd.evar -> goal - (* Instantiates a goal with an open term *) val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map |