From 79569a71ff600d118e902c9d55c311d69953bd86 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Sep 2014 14:07:09 +0200 Subject: Adding an evar version of the make_clenv function. --- proofs/clenv.mli | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'proofs/clenv.mli') diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 35bed8f40..b57178cd4 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Environ open Evd @@ -105,3 +106,33 @@ val clenv_push_prod : clausenv -> clausenv (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.std_ppcmds +(** {6 Evar version} *) + +type hole = { + hole_evar : constr; + hole_type : types; + hole_deps : bool * bool; + (** Dependent in hypotheses then in conclusion *) + hole_name : Name.t; +} + +type clause = { + cl_holes : hole list; + cl_concl : types; +} + +val make_evar_clause : env -> evar_map -> int option -> types -> + (evar_map * clause) +(** An evar version of {!make_clenv_binding}. Given a type [t], + [evar_environments env sigma n t bl] tries to eliminate at most [n] products + of the type [t] by filling it with evars. It returns the resulting type + together with the list of holes generated. Assumes that [t] is well-typed + in the environment. *) + +val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings -> + evar_map +(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained + in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in + the environment. The boolean [hyps] is a compatibility flag that allows to + consider arguments to be dependent only when they appear in hypotheses and + not in the conclusion. *) -- cgit v1.2.3