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.ml | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'kernel/context.ml')

diff --git a/kernel/context.ml b/kernel/context.ml
index 94fcfb486..fed6a5feb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -416,12 +416,24 @@ module NamedList =
   struct
     module Declaration =
       struct
-        type t = Id.t list * Constr.t option * Constr.t
-
-        let map_constr f (ids, copt, ty as decl) =
-          let copt' = Option.map f copt in
-          let ty' = f ty in
-          if copt == copt' && ty == ty' then decl else (ids, copt', ty')
+        type t =
+          | LocalAssum of Id.t list * Constr.t
+          | LocalDef of Id.t list * Constr.t * Constr.t
+
+        let map_constr f = function
+          | LocalAssum (ids, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalAssum (ids, ty')
+          | LocalDef (ids, c, ty) as decl ->
+             let ty' = f ty in
+             let c' = f c in
+             if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
+
+        let to_named_context = function
+          | LocalAssum (ids, t) ->
+             List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids
+          | LocalDef (ids, v, t) ->
+             List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids
       end
 
     type t = Declaration.t list
-- 
cgit v1.2.3