From fd1497730b5054a98007248960c4bd5639b51c81 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 26 Jan 2005 13:01:48 +0000
Subject: Ajout cas VernacBackTo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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";;
-- 
cgit v1.2.3