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 --- kernel/safe_typing.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 31bb8143e..7ca033383 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,3 +136,5 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : safe_environment -> field -> Retroknowledge.entry -> constr -> safe_environment + +val register_inline : constant -> safe_environment -> safe_environment -- cgit v1.2.3