Retour à un message d'erreur d'apply qui montre un échec sans sans réduction

de la conclusion du lemme



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

1 files changed, 22 insertions, 19 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0d643e1b53..99bb388365 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -550,25 +550,28 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl =
   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 - 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 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 try_apply thm_ty nprod =
+    let n = nb_prod thm_ty - 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 in
+  try try_apply thm_ty0 concl_nprod
+  with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
+    let rec try_red_apply thm_ty =
+      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 try_apply red_thm concl_nprod
+        with PretypeError _|RefinerError _|UserError _|Failure _ ->
+          try_red_apply red_thm
+      with Redelimination -> 
+        (* Last chance: if the head is a variable, apply may try
+	   second order unification *)
+        if concl_nprod <> 0 then try_apply thm_ty 0
+          (* Reraise the initial error message *)
+        else raise exn in
+    try_red_apply thm_ty0
 
 let apply_with_ebindings = apply_with_ebindings_gen false
 let eapply_with_ebindings = apply_with_ebindings_gen true