From 763102437580da08cd96d06d05d99dc1a3eda1b1 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 5 Apr 2001 14:29:44 +0000
Subject: mise en place de Correctness; vieille syntaxe Extraction viree de
 g_vernac.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 5 -----
 parsing/lexer.ml4    | 2 +-
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 13a9ca9fb7..0ec5584faf 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -457,11 +457,6 @@ GEXTEND Gram
       | IDENT "Reset"; IDENT "Section"; id = identarg ->
           <:ast< (ResetSection $id) >>
       
-(* Extraction *)
-      | IDENT "Extraction"; id = identarg ->
-          <:ast< (PrintExtractId $id) >>
-      | IDENT "Extraction" -> <:ast< (PrintExtract) >>
-
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >>
       |	IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >>
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 570e047116..3f1f952497 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -177,7 +177,7 @@ let get_buff len = String.sub !buff 0 len
 
 let rec ident len = parser
   | [< ' ('a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' 
-         |'\248'..'\255' | '0'..'9' | ''' | '_' as c); s >] ->
+         |'\248'..'\255' | '0'..'9' | ''' | '_' | '@' as c); s >] ->
       ident (store len c) s
   | [< >] -> len
 
-- 
cgit v1.2.3