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 --- library/global.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library/global.ml') diff --git a/library/global.ml b/library/global.ml index f120ef195..28b691769 100644 --- a/library/global.ml +++ b/library/global.ml @@ -162,4 +162,5 @@ let register field value by_clause = let senv = Safe_typing.register !global_env field entry by_clause in global_env := senv - +let register_inline c = + global_env := Safe_typing.register_inline c !global_env -- cgit v1.2.3