From e97e56bcb2e7312d27232117180dbb7bddd67fe7 Mon Sep 17 00:00:00 2001
From: mdenes
Date: Wed, 10 Jul 2013 12:22:21 +0000
Subject: Added a Register Inline command for the native compiler. Will be
 ported to the VM too. Almost only a new grammar entry since the inlining
 machinery was already implemented.

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

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7a78a7dae2..bc07fe8962 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -177,7 +177,10 @@ GEXTEND Gram
           VernacCoFixpoint (Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
-	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
+	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
+      | IDENT "Register"; IDENT "Inline"; id = identref ->
+          VernacRegister(id, RegisterInline)
+  ] ]
   ;
   gallina_ext:
     [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
-- 
cgit v1.2.3