diff options
| author |  Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-20 11:38:48 +0100 |
|---|---|---|
| committer | Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-23 11:17:10 +0100 |
| commit | 26153f161da2aa85454aece95b7a6d8cd5d446cf (patch) | |
| tree | 5f827f10baa4694d032a6bc98fa5718ed8fa543b /toplevel/vernacentries.ml | |
| parent | c01d2f47a8202e7023250e4cfbbebdac6abb3abb (diff) | |
Load: don't give anomaly on aborted proofs (Close: #3882)
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 52b4dc8cf..a4ffae0ff 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1952,14 +1952,16 @@ let interp ?proof locality poly c = | VernacComments l -> if_verbose msg_info (str "Comments ok\n") | VernacNop -> () + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm") + | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm") + | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm") + | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm") + | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm") + | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm") + (* Proof management *) | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false - | VernacAbort id -> anomaly (str "VernacAbort not handled by Stm") - | VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm") - | VernacRestart -> anomaly (str "VernacRestart not handled by Stm") - | VernacUndo _ -> anomaly (str "VernacUndo not handled by Stm") - | VernacUndoTo _ -> anomaly (str "VernacUndoTo not handled by Stm") - | VernacBacktrack _ -> anomaly (str "VernacBacktrack not handled by Stm") | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () |