From b3e1879a09c3623c7a04858a7421b316abd65293 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 27 Feb 2013 14:39:14 +0000
Subject: Minor cleanup around Term_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16253 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel/cooking.mli')

diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 03acb87a9..d6280e119 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,9 +21,13 @@ type recipe = {
   d_abstract : Sign.named_context;
   d_modlist : work_list }
 
-val cook_constant :
-  env -> recipe ->
-    constant_def * constant_type * constraints * bool * Sign.section_context
+type inline = bool
+
+type result =
+  constant_def * constant_type * constraints * inline
+    * Sign.section_context option
+
+val cook_constant : env -> recipe -> result
 
 
 (** {6 Utility functions used in module [Discharge]. } *)
-- 
cgit v1.2.3