diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |