diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:43 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:43 +0000 |
| commit | e3d3d73dfca0576cb25ce555cc445c657baecb19 (patch) | |
| tree | 0499dd493ba52659e0fd201f30a4738d355bc7c2 /proofs/proofview.ml | |
| parent | 0e24703029ecdbc87146a3bcf50faecf18a8c583 (diff) | |
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
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 7eb32f34a..bbeed4ad1 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 *) |