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
---
 printing/ppvernac.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 427317a45a..d8ddb275d1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -920,6 +920,9 @@ let rec pr_vernac = function
 	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
 	| LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid
       in str"Locate" ++ spc() ++ pr_locate loc
+  | VernacRegister (id, RegisterInline) ->
+      hov 2
+        (str "Register Inline" ++ spc() ++ pr_lident id)
   | VernacComments l ->
       hov 2
         (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l)
-- 
cgit v1.2.3