diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5dcc170b10..0e8ca22899 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2008,7 +2008,6 @@ let interp ?proof ~atts ~st c = | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index a837b77a33..0fdd2faafa 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -31,7 +31,6 @@ let rec has_Fail = function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true | _ -> false |