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.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'kernel/context.ml')

diff --git a/kernel/context.ml b/kernel/context.ml
index 4f3f649c..4a7204b7 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -43,8 +43,6 @@ struct
       | 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. *)
     let get_name = function
       | LocalAssum (na,_)
@@ -151,13 +149,16 @@ struct
       | LocalAssum (na, ty) -> na, None, ty
       | LocalDef (na, v, ty) -> na, Some v, ty
 
+    let drop_body = function
+      | LocalAssum _ as d -> d
+      | LocalDef (na, v, ty) -> LocalAssum (na, ty)
+
   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 *)
   let empty = []
@@ -192,7 +193,7 @@ struct
   let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given rel-context. *)
-  let map f = List.smartmap (Declaration.map_constr f)
+  let map f = List.Smart.map (Declaration.map_constr f)
 
   (** Perform a given action on every declaration in a given rel-context. *)
   let iter f = List.iter (Declaration.iter_constr f)
@@ -214,6 +215,8 @@ struct
       | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
     in aux [] l
 
+  let drop_bodies l = List.Smart.map Declaration.drop_body l
+
   (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
       with n = |Δ| and with the {e local definitions} of [Γ] skipped in
       [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
@@ -241,8 +244,6 @@ struct
       | 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. *)
     let get_id = function
       | LocalAssum (id,_) -> id
@@ -353,6 +354,10 @@ struct
       | id, None, ty -> LocalAssum (id, ty)
       | id, Some v, ty -> LocalDef (id, v, ty)
 
+    let drop_body = function
+      | LocalAssum _ as d -> d
+      | LocalDef (id, v, ty) -> LocalAssum (id, ty)
+
     let of_rel_decl f = function
       | Rel.Declaration.LocalAssum (na,t) ->
           LocalAssum (f na, t)
@@ -370,7 +375,6 @@ struct
       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 *)
   let empty = []
@@ -392,7 +396,7 @@ struct
   let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given named-context. *)
-  let map f = List.smartmap (Declaration.map_constr f)
+  let map f = List.Smart.map (Declaration.map_constr f)
 
   (** Perform a given action on every declaration in a given named-context. *)
   let iter f = List.iter (Declaration.iter_constr f)
@@ -409,6 +413,8 @@ struct
   let to_vars l =
     List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l
 
+  let drop_bodies l = List.Smart.map Declaration.drop_body l
+
   (** [instance_from_named_context Ω] 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
@@ -429,8 +435,6 @@ module Compacted =
           | LocalAssum of Id.t list * 'types
           | LocalDef of Id.t list * 'constr * 'types
 
-        type t = (Constr.constr, Constr.types) pt
-
         let map_constr f = function
           | LocalAssum (ids, ty) as decl ->
              let ty' = f ty in
@@ -454,7 +458,6 @@ module Compacted =
       end
 
     type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-    type t = Declaration.t list
 
     let fold f l ~init = List.fold_right f l init
   end
-- 
cgit v1.2.3