diff options
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) |