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


From 5a9e90e426ba2e25cbcb76af2bb67717984e2b6b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Oct 2020 16:48:38 +0200
Subject: [kernel] Allow to set typing flags in add_mind [inductive]

---
 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 c4d0fffe2b..287274e39a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -103,6 +103,7 @@ val add_private_constant :
 (** Adding an inductive type *)
 
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Label.t -> Entries.mutual_inductive_entry ->
     MutInd.t safe_transformer
 
-- 
cgit v1.2.3