commit d'un bug de Apply.

Avec Apply c, on essaie d'unifier le type de c avec le but courant.
Si ca echoue on essaie d'expanser la constante de tete du type du theoreme,
et essaie de faire Apply recursivement. Ca ameliore sensiblement la puissance
de Apply mais ce n'est pas 100% backward-compatible.


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

1 files changed, 16 insertions, 4 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0e454846a0..7b441e1f49 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -483,15 +483,27 @@ let bring_hyps clsl gl =
 (* Resolution with missing arguments *)
 
 let apply_with_bindings  (c,lbind) gl = 
-  let (wc,kONT) = startWalk gl in
-  let t = w_hnf_constr wc (w_type_of wc c) in 
-  let clause = make_clenv_binding_apply wc (c,t) lbind in
   let apply = 
     match kind_of_term c with 
       | IsLambda _ -> res_pf_cast 
       | _ -> res_pf 
   in 
-  apply kONT clause gl
+  let (wc,kONT) = startWalk gl in
+  let rec try_apply thm_ty =
+    try
+      let clause = make_clenv_binding_apply wc (c,thm_ty) lbind in
+      apply kONT clause gl
+    with (Logic.RefinerError _|UserError _) as exn ->
+      let ored =
+        try Some (Tacred.red_product (w_env wc) (w_Underlying wc) thm_ty)
+        with Tacred.Redelimination -> None
+      in
+      (match ored with
+          Some rty ->
+            try_apply rty
+        | None -> raise exn) in
+  try_apply (w_type_of wc c)
+
 
 let apply c = apply_with_bindings (c,[])
 let apply_com = tactic_com (fun c -> apply_with_bindings (c,[]))