diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8db615add0..dfd50c99a5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2126,7 +2126,7 @@ let rec xlate_vernac = | VernacVar _ -> xlate_error "Grammar vernac obsolete" | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _) - | VernacBack _|VernacBackTo _|VernacRestoreState _| VernacWriteState _| + | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _| VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _| VernacTacticGrammar _) -> xlate_error "TODO: vernac";; |