From 3e6bc0e8d09e3eb913b366b4f5db280154b94018 Mon Sep 17 00:00:00 2001
From: Matej Kosik <matej.kosik@inria.fr>
Date: Sun, 14 Aug 2016 19:10:35 +0200
Subject: CLEANUP: Type alias "Context.section_context" was removed

---
 kernel/cooking.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cooking.mli')

diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 327e697d2..eb4073096 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -19,7 +19,7 @@ type inline = bool
 type result =
   constant_def * constant_type * projection_body option * 
     bool * constant_universes * inline
-    * Context.section_context option
+    * Context.Named.t option
 
 val cook_constant : env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
-- 
cgit v1.2.3