diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 6 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 11 |
2 files changed, 10 insertions, 7 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a0064b13b8..56bec28db0 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -445,7 +445,7 @@ let clenv_constrain_missing_args mlist clause = (****************************************************************) (* Clausal environment for an application *) -let make_clenv_binding_gen n gls (c,t) = function +let make_clenv_binding_gen hyps_only n gls (c,t) = function | ImplicitBindings largs -> let clause = mk_clenv_from_n gls n (c,t) in clenv_constrain_dep_args (n <> None) clause largs @@ -455,8 +455,8 @@ let make_clenv_binding_gen n gls (c,t) = function | NoBindings -> mk_clenv_from_n gls n (c,t) -let make_clenv_binding_apply gls n = make_clenv_binding_gen (Some n) gls -let make_clenv_binding = make_clenv_binding_gen None +let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls +let make_clenv_binding = make_clenv_binding_gen false None (****************************************************************) (* Pretty-print *) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 53a106ade5..98950458ea 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -17,6 +17,7 @@ open Environ open Evd open Evarutil open Mod_subst +open Rawterm (*i*) (***************************************************************) @@ -93,17 +94,19 @@ val clenv_missing : clausenv -> metavariable list (* defines metas corresponding to the name of the bindings *) val clenv_match_args : - constr Rawterm.explicit_bindings -> clausenv -> clausenv + constr explicit_bindings -> clausenv -> clausenv val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv (* start with a clenv to refine with a given term with bindings *) -(* 1- the arity of the lemma is fixed *) +(* the arity of the lemma is fixed *) +(* the optional int tells how many prods of the lemma have to be used *) +(* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings -> + evar_info sigma -> int option -> constr * constr -> constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv + evar_info sigma -> constr * constr -> constr bindings -> clausenv (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where [lmetas] is a list of metas to be applied to a proof of [t] so that |