diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-25 13:02:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-25 13:02:22 +0000 |
| commit | 0def214a2e9fb473d0f137598d5ee38d36c47c86 (patch) | |
| tree | 655ee826fad9111a98b0a70333c66ecc071f1fbd /pretyping/clenv.mli | |
| parent | 8b4637c2a5ff1b6774be4f40665ccc03b687a47e (diff) | |
Correction d'une tentative incorrecte (révision 9266) de clarification
du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle
correction qui évite ce codage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.mli')
| -rw-r--r-- | pretyping/clenv.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 53a106ade..98950458e 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 |