From e3d3d73dfca0576cb25ce555cc445c657baecb19 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Mon, 4 Nov 2013 18:08:43 +0000
Subject: 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
---
 proofs/proofview.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs/proofview.ml')

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 *)
-- 
cgit v1.2.3