From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 00:02:54 +0200
Subject: Ensure statically that declarations built by Term_typing are direct.

This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
---
 kernel/safe_typing.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b9a68663d3..36ca3d8c47 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -88,7 +88,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -103,6 +102,9 @@ val add_constant :
   ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * private_constants) safe_transformer
 
+val add_recipe :
+  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
+
 (** Adding an inductive type *)
 
 val add_mind :
-- 
cgit v1.2.3