From 0def214a2e9fb473d0f137598d5ee38d36c47c86 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 25 Oct 2006 13:02:22 +0000 Subject: 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/clenv.mli | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'pretyping/clenv.mli') 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 -- cgit v1.2.3