diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index f120ef1951..28b6917697 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 diff --git a/library/global.mli b/library/global.mli index 531526846c..3238294f2e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -104,3 +104,5 @@ val env_of_context : Environ.named_context_val -> Environ.env (** spiwack: register/unregister function for retroknowledge *) val register : Retroknowledge.field -> constr -> constr -> unit + +val register_inline : constant -> unit |