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

4 files changed, 13 insertions, 10 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
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 66de55a1d8..be1d52a6c9 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -46,7 +46,7 @@ END
 
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
   let t = pf_hnf_constr gl (pf_type_of gl c) in 
-  let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in 
+  let clause = make_clenv_binding_apply gl None (c,t) lbind in 
   Clenvtac.e_res_pf clause gl
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d0e8645453..8d9d9e0308 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -518,7 +518,7 @@ let apply_with_bindings (c,lbind) gl =
     try
       let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
       if n<0 then error "Apply: theorem has not enough premisses.";
-      let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in
+      let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
       Clenvtac.res_pf clause gl
     with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
@@ -529,7 +529,7 @@ let apply_with_bindings (c,lbind) gl =
   with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) ->
     (* Last chance: if the head is a variable, apply may try
        second order unification *)
-    let clause = make_clenv_binding gl (c,thm_ty0) lbind in 
+    let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in 
     Clenvtac.res_pf clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)