diff options
| author | herbelin | 2006-10-25 13:02:22 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-25 13:02:22 +0000 |
| commit | 0def214a2e9fb473d0f137598d5ee38d36c47c86 (patch) | |
| tree | 655ee826fad9111a98b0a70333c66ecc071f1fbd /pretyping | |
| 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')
| -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 |