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 3b4af8c7ea..365c234ae3 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2112,7 +2112,7 @@ let rec xlate_vernac = | VernacVar _ -> xlate_error "Grammar vernac obsolete" | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _) - | VernacBack _|VernacRestoreState _| VernacWriteState _| + | VernacBack _|VernacBackTo _|VernacRestoreState _| VernacWriteState _| VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _| VernacTacticGrammar _) -> xlate_error "TODO: vernac";; |