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
---
 intf/vernacexpr.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 138ef5cbbe..f0f565b53d 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -203,6 +203,11 @@ type scheme =
   | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
+(* This type allows to register inline of constants in native compiler.
+   It will be extended with primitive inductive types and operators *)
+type register_kind = 
+  | RegisterInline
+
 type bullet =
     | Dash
     | Star
@@ -373,6 +378,7 @@ type vernac_expr =
   | VernacPrint of printable
   | VernacSearch of searchable * search_restriction
   | VernacLocate of locatable
+  | VernacRegister of lident * register_kind
   | VernacComments of comment list
   | VernacNop
 
-- 
cgit v1.2.3