diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-13 18:26:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:37:40 +0200 |
| commit | 0ae6d27680e5b87bbb00c6941cee1b0c309624ec (patch) | |
| tree | ddc4f3477cc698ddd0284ca7d337027c2b5c97dd /proofs/goal.mli | |
| parent | 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 (diff) | |
Goal: remove some functions from the compatibility layer.
The rest will take more work.
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 |