diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 17:48:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:39 +0100 |
| commit | 7267dfafe9215c35275a39814c8af451961e997c (patch) | |
| tree | c9b8f5f882aa92e529c4ce0789a8a9981efc2689 /proofs/goal.mli | |
| parent | 536026f3e20f761e8ef366ed732da7d3b626ac5e (diff) | |
Goal API using EConstr.
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index 6a79c1f45..ca6584e76 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -38,7 +38,7 @@ module V82 : sig val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val (* Access to ".evar_concl" *) - val concl : Evd.evar_map -> goal -> Term.constr + val concl : Evd.evar_map -> goal -> EConstr.constr (* Access to ".evar_extra" *) val extra : Evd.evar_map -> goal -> Evd.Store.t @@ -48,16 +48,16 @@ module V82 : sig the evar corresponding to the goal, and an updated evar_map. *) val mk_goal : Evd.evar_map -> Environ.named_context_val -> - Term.constr -> + EConstr.constr -> Evd.Store.t -> - goal * Term.constr * Evd.evar_map + goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map + val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map (* Instantiates a goal with an open term, reusing name of goal for second goal *) - val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map + val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map (* Principal part of the weak-progress tactical *) val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool |