Fix the tactical ; [ … ] : the "incorrect number of goal" error was not caught by ltac tacticals.

The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad).

Spotted in ProjectiveGeometry and Goedel.

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

3 files changed, 24 insertions, 11 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 7eb32f34a2..bbeed4ad10 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -460,8 +460,10 @@ let tclEXTEND tacs1 rtac tacs2 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun step ->
-  let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
-  tclDISPATCH tacs
+  try
+    let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
+    tclDISPATCH tacs
+  with SizeMismatch -> tclZERO SizeMismatch
 
 let tclINDEPENDENT tac =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2945fb7141..8bd7b8a283 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -179,7 +179,11 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
    goal (starting with the first goal). In the case of [tclDISPATCHL],
    the tactic returns a list of the same size as the argument list (of
    tactics), each element being the result of the tactic executed in
-   the corresponding goal. *)
+   the corresponding goal.
+
+   When the length of the tactic list is not the number of goal,
+   raises [SizeMismatch] *)
+exception SizeMismatch
 val tclDISPATCH : unit tactic list -> unit tactic
 val tclDISPATCHL : 'a tactic list -> 'a list tactic
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 299a1e1768..bcb6041eff 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -415,24 +415,31 @@ module New = struct
 
   let tclTHENS3PARTS t1 l1 repeat l2 =
     tclINDEPENDENT begin
-      t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2)
+      t1 <*>
+        Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
+          begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end
+          begin function
+            | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals")
+            | reraise -> tclZERO reraise
+          end
     end
   let tclTHENSFIRSTn t1 l repeat =
     tclTHENS3PARTS t1 l repeat [||]
   let tclTHENFIRSTn t1 l =
     tclTHENSFIRSTn t1 l (tclUNIT())
   let tclTHENFIRST t1 t2 =
-    tclEXTEND [] begin
-      t1 <*> tclFOCUS 1 1 t2
-    end []
+    tclTHENFIRSTn t1 [|t2|]
   let tclTHENLASTn t1 l =
-    tclINDEPENDENT begin
-      t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l)
-    end
+    tclTHENS3PARTS t1 [||] (tclUNIT()) l
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
   let tclTHENS t l =
     tclINDEPENDENT begin
-      t <*> tclDISPATCH l
+      t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
+          begin tclDISPATCH l end
+          begin function
+            | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals")
+            | reraise -> tclZERO reraise
+          end
     end
   let tclTHENLIST l =
     List.fold_left tclTHEN (tclUNIT()) l