From b19ad7d1dbd431975c1718c08f8ebd38c5b5f376 Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 19 May 2005 11:54:42 +0000
Subject: added VernacBacktrack (new backtracking command dedicated to
 interfaces like PG, coqied or pcoq) in order to get rid of a pattern matching
 not exhaustive.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7038 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 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";;
-- 
cgit v1.2.3