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
---
 toplevel/vernacentries.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 526aa9230f..bac1fcd488 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1513,6 +1513,16 @@ let vernac_locate = function
   | LocateTactic qid -> print_located_tactic qid
   | LocateFile f -> msg_notice (locate_file f)
 
+let vernac_register id r =
+ if Pfedit.refining () then
+    error "Cannot register a primitive while in proof editing mode.";
+  let t = (Constrintern.global_reference (snd id)) in
+  if not (isConst t) then
+    error "Register inline: a constant is expected";
+  let kn = destConst t in
+  match r with
+  | RegisterInline -> Global.register_inline kn
+
 (****************)
 (* Backtracking *)
 
@@ -1823,6 +1833,7 @@ let interp locality c = match c with
   | VernacPrint p -> vernac_print p
   | VernacSearch (s,r) -> vernac_search s r
   | VernacLocate l -> vernac_locate l
+  | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
   | VernacNop -> ()
 
-- 
cgit v1.2.3