From 1297523bffdc3a9fe3e447acc6837be835e86d06 Mon Sep 17 00:00:00 2001
From: Matej Kosik <matej.kosik@inria.fr>
Date: Mon, 15 Aug 2016 14:14:14 +0200
Subject: CLEANUP: changing the definition of the
 "Context.NamedList.Declaration" type

---
 kernel/context.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/context.mli')

diff --git a/kernel/context.mli b/kernel/context.mli
index c5da51381..72fbfb540 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -255,8 +255,12 @@ module NamedList :
 sig
   module Declaration :
   sig
-    type t = Id.t list * Constr.t option * Constr.t
+    type t =
+      | LocalAssum of Id.t list * Constr.t
+      | LocalDef of Id.t list * Constr.t * Constr.t
+
     val map_constr : (Constr.t -> Constr.t) -> t -> t
+    val to_named_context : t -> Named.t
   end
 
   type t = Declaration.t list
-- 
cgit v1.2.3