Uses Proofview.tclEXTEND more sparingly.

It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than
at each tclTHEN. Hopefully avoiding making things a bit less slow.

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

3 files changed, 46 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 548fcf00b..c770df051 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1428,15 +1428,19 @@ let intro_register dbg kont db =
 
 let search d n mod_delta db_list local_db =
   let rec search d n local_db =
-    if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
-      Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
-	(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
-	   ( Goal.concl >>- fun concl ->
-	     let d' = incr_dbg d in
-	     Tacticals.New.tclFIRST
-	       (List.map
-		  (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-		  (possible_resolve d mod_delta db_list local_db concl))))
+    (* spiwack: the test of [n] to 0 must be done independently in
+       each goal. Hence the [tclEXTEND] *)
+    Proofview.tclEXTEND [] begin
+      if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+        Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
+	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
+	     ( Goal.concl >>- fun concl ->
+	       let d' = incr_dbg d in
+	       Tacticals.New.tclFIRST
+	         (List.map
+		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
+		    (possible_resolve d mod_delta db_list local_db concl))))
+    end []
   in
   search d n local_db
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ee89b55a8..412ed119f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -373,7 +373,7 @@ module New = struct
   open Proofview.Notations
 
   let tclTHEN t1 t2 =
-    t1 <*> tclEXTEND [] t2 []
+    t1 <*> t2
 
   let tclFAIL lvl msg =
     tclZERO (Refiner.FailError (lvl,lazy msg))
@@ -384,27 +384,37 @@ module New = struct
       tclUNIT ()
     with e -> tclZERO e
   let tclORELSE0 t1 t2 =
-    tclORELSE
-      t1
-      begin fun e ->
-        catch_failerror e <*> t2
-      end
+    tclEXTEND [] begin
+      tclORELSE
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2
+        end
+    end []
   let tclORELSE t1 t2 =
     tclORELSE0 (tclPROGRESS t1) t2
 
   let tclTHENS3PARTS t1 l1 repeat l2 =
-    t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2)
+    tclEXTEND [] begin
+      t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2)
+    end []
   let tclTHENSFIRSTn t1 l repeat =
     tclTHENS3PARTS t1 l repeat [||]
   let tclTHENFIRSTn t1 l =
     tclTHENSFIRSTn t1 l (tclUNIT())
   let tclTHENFIRST t1 t2 =
-    t1 <*> tclFOCUS 1 1 t2
+    tclEXTEND [] begin
+      t1 <*> tclFOCUS 1 1 t2
+    end []
   let tclTHENLASTn t1 l =
-    t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l)
+    tclEXTEND [] begin
+      t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l)
+    end []
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
   let tclTHENS t l =
-    t <*> tclDISPATCH l
+    tclEXTEND [] begin
+      t <*> tclDISPATCH l
+    end []
   let tclTHENLIST l =
     List.fold_left tclTHEN (tclUNIT()) l
 
@@ -417,9 +427,11 @@ module New = struct
     tclORELSE0 t (tclUNIT ())
 
   let tclIFTHENELSE t1 t2 t3 =
-    tclIFCATCH t1
-      (fun () -> tclEXTEND [] t2 [])
-      (fun _ -> t3)
+    tclEXTEND [] begin
+      tclIFCATCH t1
+        (fun () -> t2)
+        (fun _ -> t3)
+    end []
   let tclIFTHENSVELSE t1 a t3 =
     tclIFCATCH t1
       (fun () -> tclDISPATCH (Array.to_list a))
@@ -448,9 +460,11 @@ module New = struct
     else tclTHEN t (tclDO (n-1) t)
 
   let rec tclREPEAT0 t =
-    tclIFCATCH t
-      (fun () -> tclEXTEND [] (tclREPEAT0 t) [])
-      (fun _ -> tclUNIT ())
+    tclEXTEND [] begin
+      tclIFCATCH t
+        (fun () -> tclREPEAT0 t)
+        (fun _ -> tclUNIT ())
+    end []
   let tclREPEAT t =
     tclREPEAT0 (tclPROGRESS t)
   let rec tclREPEAT_MAIN0 t =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 58aff5fdb..d32a0dab7 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -183,8 +183,8 @@ module New : sig
      (meaning that it will jump over [n] error catching tacticals FROM
      THIS MODULE. *)
   val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
-  val tclORELSE0 : 'a tactic -> 'a tactic -> 'a tactic
-  val tclORELSE  : 'a tactic -> 'a tactic -> 'a tactic
+  val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
+  val tclORELSE  : unit tactic -> unit tactic -> unit tactic
 
   (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|]
       gls] applies the tactic [tac1] to [gls] then, applies [t1], ...,
@@ -209,7 +209,7 @@ module New : sig
   val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic
 
   val tclTRY : unit tactic -> unit tactic
-  val tclFIRST : 'a tactic list -> 'a tactic
+  val tclFIRST : unit tactic list -> unit tactic
   val tclFIRST_PROGRESS_ON : ('a -> unit tactic) -> 'a list -> unit tactic
   val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
   val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic