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 /myocamlbuild.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 'myocamlbuild.ml')
0 files changed, 0 insertions, 0 deletions