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

2 files changed, 9 insertions, 3 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