From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 parsing/g_proofs.ml4 | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'parsing/g_proofs.ml4')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0a48748f..05878e97 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_proofs.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+(* $Id: g_proofs.ml4 10628 2008-03-06 14:56:08Z msozeau $ *)
+
 
 open Pcoq
 open Pp
@@ -59,6 +62,7 @@ GEXTEND Gram
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
+      | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
       | IDENT "Focus" -> VernacFocus None
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
@@ -101,7 +105,8 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+    [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> 
+          HintsResolve (List.map (fun x -> (n, x)) lc)
       | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
-- 
cgit v1.2.3