From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 kernel/context.mli | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

(limited to 'kernel/context.mli')

diff --git a/kernel/context.mli b/kernel/context.mli
index c97db434..2b0d36cb 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
 
@@ -87,13 +85,15 @@ sig
     val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
 
     val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't
+
+    (** Turn [LocalDef] into [LocalAssum], identity otherwise. *)
+    val drop_body : ('c, 't) pt -> ('c, 't) pt
   end
 
   (** Rel-context is represented as a list of declarations.
       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
@@ -132,6 +132,9 @@ sig
       and each {e local definition} is mapped to [false]. *)
   val to_tags : ('c, 't) pt -> bool list
 
+  (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *)
+  val drop_bodies : ('c, 't) pt -> ('c, 't) pt
+
   (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
       with n = |Δ| and with the {e local definitions} of [Γ] skipped in
       [args] where [mk] is used to build the corresponding variables.
@@ -153,8 +156,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
 
@@ -207,6 +208,9 @@ sig
     val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't
     val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt
 
+    (** Turn [LocalDef] into [LocalAssum], identity otherwise. *)
+    val drop_body : ('c, 't) pt -> ('c, 't) pt
+
     (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value.
         The function provided as the first parameter determines how to translate "names" to "ids". *)
     val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt
@@ -220,7 +224,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
@@ -255,6 +258,9 @@ sig
   (** Return the set of all identifiers bound in a given named-context. *)
   val to_vars : ('c, 't) pt -> Id.Set.t
 
+  (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *)
+  val drop_bodies : ('c, 't) pt -> ('c, 't) pt
+
   (** [to_instance Ω] builds an instance [args] such
       that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
       definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
@@ -270,15 +276,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