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_decl_mode.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'parsing/g_decl_mode.ml4')

diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 5c7b40af..61c3474d 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -6,8 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
+(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+
 
 open Decl_expr
 open Names
@@ -28,7 +31,6 @@ GLOBAL: proof_instr;
   thesis :
     [[ "thesis" -> Plain 
      | "thesis"; "for"; i=ident -> (For i)
-     | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n))
      ]];
   statement :
     [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
-- 
cgit v1.2.3