diff options
| author | aspiwack | 2013-11-02 15:36:45 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:36:45 +0000 |
| commit | 07569af8e7528fc63b93824edd5253e8a92fc2c0 (patch) | |
| tree | 98dc680c84328710e07c4fe6b9780600f01baf1f /toplevel | |
| parent | 49762f64a3616919dbfc1be09410cf830d168e70 (diff) | |
Fixes parsing of all: followed by a typechecking/evaluation command.
Exceptions raised during parsing are caught by the parser and result in weird
parsing behaviour. Instead I added a special case in vernac_expr which always
raises an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac_classifier.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 3c19e887c1..139dc67d7a 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -83,7 +83,7 @@ let rec classify_vernac e = | VernacBullet _ | VernacFocus _ | VernacUnfocus _ | VernacSubproof _ | VernacEndSubproof _ - | VernacSolve _ + | VernacSolve _ | VernacError _ | VernacCheckGuard _ | VernacUnfocused _ | VernacSolveExistential _ -> VtProofStep, VtLater diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f3298c29b9..7655d3032d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1592,6 +1592,8 @@ let interp ?proof locality c = | VernacTimeout _ -> assert false | VernacStm _ -> assert false + | VernacError e -> raise e + (* Syntax *) | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e) |