Suite unification apply et eapply (l'un et l'autre profite maintenant

de la réduction paresseuse du lemme [eapply n'en profitait pas], et
l'un et l'autre profite de l'unification2nd ordre sur la forme réduite
du lemme [apply n'en profitait pas]).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9771 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 20 insertions, 28 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ad31f5d3b..310b70fd9 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -44,13 +44,6 @@ TACTIC EXTEND eassumption
 | [ "eassumption" ] -> [ e_assumption ]
 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 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
-			     
 TACTIC EXTEND eexact
 | [ "eexact" constr(c) ] -> [ e_give_exact c ]
 END
@@ -66,7 +59,7 @@ TACTIC EXTEND eapply
   [ "eapply" constr_with_bindings(c) ] -> [ Tactics.eapply_with_bindings c ]
 END
 
-let vernac_e_resolve_constr c = h_eapply (c,NoBindings)
+let simplest_eapply c = h_eapply (c,NoBindings)
 
 let e_constructor_tac boundopt i lbind gl = 
     let cl = pf_concl gl in 
@@ -82,7 +75,7 @@ let e_constructor_tac boundopt i lbind gl =
     | None -> ()
   end;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in
+  let apply_tac = eapply_with_bindings (cons,lbind) in
   (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
 ; intros; apply_tac]) gl
 
@@ -137,8 +130,8 @@ END
 
 let one_step l gl =
   [Tactics.intro]
-  @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map e_resolve_constr l)
+  @ (List.map simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map simplest_eapply l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
@@ -169,7 +162,7 @@ open Auto
 let unify_e_resolve  (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in
-  vernac_e_resolve_constr c gls
+  simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 4621088e2..d17afd293 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -22,10 +22,6 @@ val e_assumption : tactic
 
 val registered_e_assumption : tactic
 
-val e_resolve_constr :  constr -> tactic
-
-val vernac_e_resolve_constr :  constr -> tactic
-
 val e_give_exact_constr : constr -> tactic
 
 val gen_eauto : bool -> bool * int -> constr list -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5a5e8989e..c496ffe64 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -42,6 +42,7 @@ open Tacexpr
 open Decl_kinds
 open Evarutil
 open Indrec
+open Pretype_errors
 
 exception Bound
 
@@ -514,24 +515,26 @@ let apply_with_bindings_gen with_evars (c,lbind) gl =
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
   let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+  let concl_nprod = nb_prod (pf_concl gl) in
   let rec try_apply thm_ty =
     try
-      let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
+      let n = nb_prod thm_ty - concl_nprod in
       if n<0 then error "Apply: theorem has not enough premisses.";
       let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
       if with_evars then Clenvtac.e_res_pf clause gl
       else Clenvtac.res_pf clause gl
-    with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
-      let red_thm =
-        try red_product (pf_env gl) (project gl) thm_ty
-        with (Redelimination | UserError _) -> raise exn in
-      try_apply red_thm in
-  try try_apply thm_ty0
-  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_apply gl None (c,thm_ty0) lbind in 
-    Clenvtac.res_pf clause gl
+    with PretypeError _|RefinerError _|UserError _|Failure _ ->
+    try 
+      (* Try to head-reduce the conclusion of the theorem *)
+      let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
+      try_apply red_thm
+    with Redelimination -> 
+      (* Last chance: if the head is a variable, apply may try
+	 second order unification *)
+      let clause = make_clenv_binding_apply gl None (c,thm_ty) lbind in 
+      if with_evars then Clenvtac.e_res_pf clause gl
+      else Clenvtac.res_pf clause gl in
+  try_apply thm_ty0
 
 let apply_with_bindings = apply_with_bindings_gen false
 let eapply_with_bindings = apply_with_bindings_gen true