From 79b6291ccda61f631aa2cfec9a12d6ea2a34fa96 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 18:01:16 +0000
Subject: Modules and ppvernac, sequel of Enrico's commit 16261

 After some investigation, I see no reason to try to hack
 the nametab in ppvernac, since everything happens there
 at a lower level (constr_expr). So the offending code that
 Enrico protected with a State.with_state_protection is now gone.

 By the way, moved some types from Declaremods to Vernacexpr
 to avoid some dependencies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c3d9438dea..5787186ad0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -222,9 +222,9 @@ GEXTEND Gram
       | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ]
   ;
   inline:
-    [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i)
-      | IDENT "Inline" -> Some (Flags.get_inline_level())
-      | -> None] ]
+    [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
+      | IDENT "Inline" -> DefaultInline
+      | -> NoInline] ]
   ;
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)
-- 
cgit v1.2.3