From 93aa8aad110a2839d16dce53af12f0728b59ed2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 14 May 2019 20:27:24 +0200
Subject: Merge the definition of constants and private constants in the API.

---
 kernel/safe_typing.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75375812c0..f2e7cff8ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -797,7 +797,7 @@ let export_private_constants ~in_section ce senv =
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_constant ~in_section l decl senv =
+let add_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
@@ -822,7 +822,11 @@ let add_constant ~in_section l decl senv =
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  kn, senv
+  let eff = match role with
+  | None -> empty_private_constants
+  | Some role -> private_constant senv role kn
+  in
+  (kn, eff), senv
 
 (** Insertion of inductive types *)
 
-- 
cgit v1.2.3