From b78f6424d9fa5a8027c4acb21b3e57ee6294bc5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 25 Jun 2020 16:43:08 +0200 Subject: [kernel] Allow to set typing flags in add_constant This is just an experiment, but makes the uses of the API easier as we don't mess with the global state anymore. --- kernel/safe_typing.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6fa9022906..c4d0fffe2b 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -93,6 +93,7 @@ val export_private_constants : (** returns the main constant *) val add_constant : + ?typing_flags:Declarations.typing_flags -> Label.t -> global_declaration -> Constant.t safe_transformer (** Similar to add_constant but also returns a certificate *) -- cgit v1.2.3