From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 27 Mar 2018 02:37:19 +0200
Subject: Swapping Context and Constr: defining declarations on constr in
 Constr.

This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.

Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
---
 kernel/context.mli | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'kernel/context.mli')

diff --git a/kernel/context.mli b/kernel/context.mli
index c97db4348e..957ac4b3d6 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -35,8 +35,6 @@ sig
     | LocalAssum of Name.t * 'types            (** name, type *)
     | LocalDef of Name.t * 'constr * 'types   (** name, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the name bound by a given declaration. *)
     val get_name : ('c, 't) pt -> Name.t
 
@@ -93,7 +91,6 @@ sig
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty rel-context *)
   val empty : ('c, 't) pt
@@ -153,8 +150,6 @@ sig
       | LocalAssum of Id.t * 'types             (** identifier, type *)
       | LocalDef of Id.t * 'constr * 'types    (** identifier, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the identifier bound by a given declaration. *)
     val get_id : ('c, 't) pt -> Id.t
 
@@ -220,7 +215,6 @@ sig
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty named-context *)
   val empty : ('c, 't) pt
@@ -270,15 +264,12 @@ sig
       | LocalAssum of Id.t list * 'types
       | LocalDef of Id.t list * 'constr * 'types
 
-    type t = (Constr.constr, Constr.types) pt
-
     val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
     val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt
     val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt
   end
 
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
 end
-- 
cgit v1.2.3