Autoriser Apply avec un but sous forme d'implication ou de quantification

universelle


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

2 files changed, 28 insertions, 11 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 38bb22342..24beccf3b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -42,7 +42,7 @@ let registered_e_assumption gl =
 let e_resolve_with_bindings_tac  (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 clause = make_clenv_binding_apply wc (-1) (c,t) lbind in 
   e_res_pf kONT clause gl
 
 let e_resolve_with_bindings = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bb34e96de..5ef73e5c4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -33,6 +33,15 @@ open Coqlib
 
 exception Bound
 
+let rec nb_prod x =
+  let rec count n c =
+    match kind_of_term c with
+        IsProd(_,_,t) -> count (n+1) t
+      | IsLetIn(_,a,_,t) -> count n (subst1 a t)
+      | IsCast(c,_) -> count n c
+      | _ -> n
+  in count 0 x
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -482,6 +491,7 @@ let bring_hyps clsl gl =
 
 (* Resolution with missing arguments *)
 
+
 let apply_with_bindings  (c,lbind) gl = 
   let apply = 
     match kind_of_term c with 
@@ -489,20 +499,27 @@ let apply_with_bindings  (c,lbind) gl =
       | _ -> res_pf 
   in 
   let (wc,kONT) = startWalk gl in
+  (* The actual type of the theorem. It will be matched against the
+  goal. If this fails, then the head constant will be unfolded step by
+  step. *)
+  let thm_ty0 = (w_type_of wc c) in
   let rec try_apply thm_ty =
     try
-      let clause = make_clenv_binding_apply wc (c,thm_ty) lbind in
+      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 wc n (c,thm_ty) lbind in
       apply kONT clause gl
     with (RefinerError _|UserError _|Failure _) 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 red_thm =
+        try red_product (w_env wc) (w_Underlying wc) thm_ty
+        with (Redelimination | UserError _) -> raise exn in
+      try_apply red_thm in
+  try try_apply thm_ty0
+  with (RefinerError _|UserError _|Failure _) ->
+    (* Last chance: if the head is a variable, apply may try
+       second order unification *)
+    let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in 
+    apply kONT clause gl
 
 
 let apply c = apply_with_bindings (c,[])