1 files changed, 197 insertions, 366 deletions

diff --git a/checker/univ.ml b/checker/univ.ml
index 668f3a05..1619010c 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
@@ -29,114 +31,6 @@ open Util
    union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
-module type Hashconsed =
-sig
-  type t
-  val hash : t -> int
-  val eq : t -> t -> bool
-  val hcons : t -> t
-end
-
-module HashedList (M : Hashconsed) :
-sig
-  type t = private Nil | Cons of M.t * int * t
-  val nil : t
-  val cons : M.t -> t -> t
-end =
-struct
-  type t = Nil | Cons of M.t * int * t
-  module Self =
-  struct
-    type _t = t
-    type t = _t
-    type u = (M.t -> M.t)
-    let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let eq l1 l2 = match l1, l2 with
-    | Nil, Nil -> true
-    | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
-    | _ -> false
-    let hashcons hc = function
-    | Nil -> Nil
-    | Cons (x, h, l) -> Cons (hc x, h, l)
-  end
-  module Hcons = Hashcons.Make(Self)
-  let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons
-  (** No recursive call: the interface guarantees that all HLists from this
-      program are already hashconsed. If we get some external HList, we can
-      still reconstruct it by traversing it entirely. *)
-  let nil = Nil
-  let cons x l =
-    let h = M.hash x in
-    let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in
-    let h = Hashset.Combine.combine h hl in
-    hcons (Cons (x, h, l))
-end
-
-module HList = struct
-
-  module type S = sig
-    type elt
-    type t = private Nil | Cons of elt * int * t
-    val hash : t -> int
-    val nil : t
-    val cons : elt -> t -> t
-    val tip : elt -> t
-    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-    val map : (elt -> elt) -> t -> t
-    val smartmap : (elt -> elt) -> t -> t
-    val exists : (elt -> bool) -> t -> bool
-    val for_all : (elt -> bool) -> t -> bool
-    val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
-    val remove : elt -> t -> t
-    val to_list : t -> elt list
-  end
-
-  module Make (H : Hashconsed) : S with type elt = H.t =
-  struct
-  type elt = H.t
-  include HashedList(H)
-
-  let hash = function Nil -> 0 | Cons (_, h, _) -> h
-
-  let tip e = cons e nil
-
-  let rec fold f l accu = match l with
-  | Nil -> accu
-  | Cons (x, _, l) -> fold f l (f x accu)
-
-  let rec map f = function
-  | Nil -> nil
-  | Cons (x, _, l) -> cons (f x) (map f l)
-
-  let smartmap = map
-  (** Apriori hashconsing ensures that the map is equal to its argument *)
-
-  let rec exists f = function
-  | Nil -> false
-  | Cons (x, _, l) -> f x || exists f l
-
-  let rec for_all f = function
-  | Nil -> true
-  | Cons (x, _, l) -> f x && for_all f l
-
-  let rec for_all2 f l1 l2 = match l1, l2 with
-  | Nil, Nil -> true
-  | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2
-  | _ -> false
-
-  let rec to_list = function
-  | Nil -> []
-  | Cons (x, _, l) -> x :: to_list l
-
-  let rec remove x = function
-  | Nil -> nil
-  | Cons (y, _, l) ->
-    if H.eq x y then l
-    else cons y (remove x l)
-
-  end
-end
-
 module RawLevel =
 struct
   open Names
@@ -174,24 +68,6 @@ struct
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
 
-  let hequal x y =
-    x == y ||
-      match x, y with
-      | Prop, Prop -> true
-      | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
-        n == n' && d == d'
-      | Var n, Var n' -> n == n'
-      | _ -> false
-
-  let hcons = function
-    | Prop as x -> x
-    | Set as x -> x
-    | Level (n,d) as x -> 
-      let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (n,d')
-    | Var n as x -> x
-
   open Hashset.Combine
 
   let hash = function
@@ -223,24 +99,7 @@ module Level = struct
 
   let data x = x.data
 
-  (** Hashcons on levels + their hash *)
-
-  module Self = struct
-    type _t = t
-    type t = _t
-    type u = unit
-    let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
-    let hash x = x.hash
-    let hashcons () x =
-      let data' = RawLevel.hcons x.data in
-      if x.data == data' then x else { x with data = data' }
-  end
-
-  let hcons =
-    let module H = Hashcons.Make(Self) in
-    Hashcons.simple_hcons H.generate H.hcons ()
-
-  let make l = hcons { hash = RawLevel.hash l; data = l }
+  let make l = { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
@@ -277,7 +136,7 @@ module Level = struct
 
   let pr u = str (to_string u)
 
-  let make m n = make (Level (n, Names.DirPath.hcons m))
+  let make m n = make (Level (n, m))
 
 end
 
@@ -310,48 +169,12 @@ struct
   module Expr = 
   struct
     type t = Level.t * int
-    type _t = t
 	
-    (* Hashing of expressions *)
-    module ExprHash = 
-    struct
-      type t = _t
-      type u = Level.t -> Level.t
-      let hashcons hdir (b,n as x) = 
-	let b' = hdir b in 
-	  if b' == b then x else (b',n)
-      let eq l1 l2 =
-        l1 == l2 || 
-        match l1,l2 with
-	| (b,n), (b',n') -> b == b' && n == n'
-
-      let hash (x, n) = n + Level.hash x
-
-    end
-
-    module HExpr =
-    struct
-
-      module H = Hashcons.Make(ExprHash)
-
-      type t = ExprHash.t
-
-      let hcons =
-        Hashcons.simple_hcons H.generate H.hcons Level.hcons
-      let hash = ExprHash.hash
-      let eq x y = x == y ||
-        (let (u,n) = x and (v,n') = y in
-           Int.equal n n' && Level.equal u v)
-
-    end
+    let make l = (l, 0)
 
-    let hcons = HExpr.hcons
-
-    let make l = hcons (l, 0)
-
-    let prop = make Level.prop
-    let set = make Level.set
-    let type1 = hcons (Level.set, 1)
+    let prop = (Level.prop, 0)
+    let set = (Level.set, 0)
+    let type1 = (Level.set, 1)
 
     let is_prop = function
       | (l,0) -> Level.is_prop l
@@ -361,22 +184,15 @@ struct
       (let (u,n) = x and (v,n') = y in
 	 Int.equal n n' && Level.equal u v)
 
-    let leq (u,n) (v,n') =
-      let cmp = Level.compare u v in
-	if Int.equal cmp 0 then n <= n'
-	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
-	else false
-
     let successor (u,n) =
       if Level.is_prop u then type1
-      else hcons (u, n + 1)
+      else (u, n + 1)
 
     let addn k (u,n as x) = 
       if k = 0 then x 
       else if Level.is_prop u then
-	hcons (Level.set,n+k)
-      else hcons (u,n+k)
+	(Level.set,n+k)
+      else (u,n+k)
 	
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
@@ -401,31 +217,29 @@ struct
       let v' = f v in 
 	if v' == v then x
 	else if Level.is_prop v' && n != 0 then
-	  hcons (Level.set, n)
-	else hcons (v', n)
+	  (Level.set, n)
+	else (v', n)
 
   end
-    
-  module Huniv = HList.Make(Expr.HExpr)
-  type t = Huniv.t
-  open Huniv
-    
-  let equal x y = x == y || 
-    (Huniv.hash x == Huniv.hash y && 
-       Huniv.for_all2 Expr.equal x y)
 
-  let make l = Huniv.tip (Expr.make l)
-  let tip x = Huniv.tip x
-    
+  type t = Expr.t list
+
+  let tip u = [u]
+  let cons u v = u :: v
+
+  let equal x y = x == y || List.equal Expr.equal x y
+
+  let make l = tip (Expr.make l)
+
   let pr l = match l with
-    | Cons (u, _, Nil) -> Expr.pr u
+    | [u] -> Expr.pr u
     | _ -> 
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma Expr.pr (to_list l)) ++
+	(prlist_with_sep pr_comma Expr.pr l) ++
         str ")"
 
   let level l = match l with
-    | Cons (l, _, Nil) -> Expr.level l
+    | [l] -> Expr.level l
     | _ -> None
 
   (* The lower predicative level of the hierarchy that contains (impredicative)
@@ -445,16 +259,16 @@ struct
   (* Returns the formal universe that lies juste above the universe variable u.
      Used to type the sort u. *)
   let super l = 
-    Huniv.map (fun x -> Expr.successor x) l
+    List.map (fun x -> Expr.successor x) l
 
   let addn n l =
-    Huniv.map (fun x -> Expr.addn n x) l
+    List.map (fun x -> Expr.addn n x) l
 
   let rec merge_univs l1 l2 =
     match l1, l2 with
-    | Nil, _ -> l2
-    | _, Nil -> l1
-    | Cons (h1, _, t1), Cons (h2, _, t2) ->
+    | [], _ -> l2
+    | _, [] -> l1
+    | h1 :: t1, h2 :: t2 ->
       (match Expr.super h1 h2 with
       | Inl true (* h1 < h2 *) -> merge_univs t1 l2
       | Inl false -> merge_univs l1 t2
@@ -466,28 +280,28 @@ struct
   let sort u =
     let rec aux a l = 
       match l with
-      | Cons (b, _, l') ->
+      | b :: l' ->
         (match Expr.super a b with
 	| Inl false -> aux a l'
 	| Inl true -> l
 	| Inr c ->
 	  if c <= 0 then cons a l
 	  else cons b (aux a l'))
-      | Nil -> cons a l
+      | [] -> cons a l
     in 
-      fold (fun a acc -> aux a acc) u nil
+      List.fold_right (fun a acc -> aux a acc) u []
 	
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y
 
-  let empty = nil
+  let empty = []
 
-  let exists = Huniv.exists
+  let exists = List.exists
 
-  let for_all = Huniv.for_all
+  let for_all = List.for_all
 
-  let smartmap = Huniv.smartmap
+  let smartmap = List.smartmap
 
 end
 
@@ -552,7 +366,7 @@ let repr g u =
     let a =
       try UMap.find u g
       with Not_found -> anomaly ~label:"Univ.repr"
-	  (str"Universe " ++ Level.pr u ++ str" undefined")
+	  (str"Universe " ++ Level.pr u ++ str" undefined.")
     in
     match a with
       | Equiv v -> repr_rec v
@@ -775,9 +589,9 @@ let check_equal_expr g x y =
 
 let check_eq_univs g l1 l2 =
   let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in
-    Huniv.for_all (fun x1 -> exists x1 l2) l1
-    && Huniv.for_all (fun x2 -> exists x2 l1) l2
+  let exists x1 l = List.exists (fun x2 -> f x1 x2) l in
+    List.for_all (fun x1 -> exists x1 l2) l1
+    && List.for_all (fun x2 -> exists x2 l1) l2
 
 let check_eq g u v =
   Universe.equal u v || check_eq_univs g u v
@@ -791,11 +605,11 @@ let check_smaller_expr g (u,n) (v,m) =
     | _ -> false
 
 let exists_bigger g ul l =
-  Huniv.exists (fun ul' -> 
+  Universe.exists (fun ul' -> 
     check_smaller_expr g ul ul') l
 
 let real_check_leq g u v =
-  Huniv.for_all (fun ul -> exists_bigger g ul v) u
+  Universe.for_all (fun ul -> exists_bigger g ul v) u
     
 let check_leq g u v =
   Universe.equal u v ||
@@ -855,7 +669,7 @@ let merge g arcu arcv =
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
       match between g arcu arcv with
-      | [] -> anomaly (str "Univ.between")
+      | [] -> anomaly (str "Univ.between.")
       | arc::rest ->
         let (max_rank, old_max_rank, best_arc, rest) =
           List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
@@ -918,7 +732,7 @@ let enforce_univ_eq u v g =
       | FastLT -> error_inconsistency Eq u v
       | FastLE -> merge g arcv arcu
       | FastNLE -> merge_disc g arcu arcv
-      | FastEQ -> anomaly (Pp.str "Univ.compare"))
+      | FastEQ -> anomaly (Pp.str "Univ.compare."))
 
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -931,7 +745,7 @@ let enforce_univ_leq u v g =
     | FastLT -> error_inconsistency Le u v
     | FastLE  -> merge g arcv arcu
     | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
+    | FastEQ -> anomaly (Pp.str "Univ.compare.")
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
@@ -944,7 +758,7 @@ let enforce_univ_lt u v g =
     | FastNLE ->
       match fast_compare_neq false g arcv arcu with
 	FastNLE -> fst (setlt g arcu arcv)
-      | FastEQ -> anomaly (Pp.str "Univ.compare")
+      | FastEQ -> anomaly (Pp.str "Univ.compare.")
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
@@ -975,7 +789,23 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
+
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+end
 
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
@@ -990,41 +820,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-let constraint_add_leq v u c =
-  (* We just discard trivial constraints like u<=u *)
-  if Expr.equal v u then c
-  else 
-    match v, u with
-    | (x,n), (y,m) -> 
-    let j = m - n in
-      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
-	Constraint.add (x,Lt,y) c
-      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.equal x y then (* u+(k+1) <= u *)
-	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
-      else if j = 0 then
-	Constraint.add (x,Le,y) c
-      else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.equal x y then c (* u <= u+k, trivial *)
-	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
-	  
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v = 
-  Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
-  match v with
-  | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) ->
-    Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
-
-let enforce_leq u v c =
-  if check_univ_leq u v then c
-  else enforce_leq u v c
-
 let check_constraint g (l,d,r) =
   match d with
   | Eq -> check_equal g l r
@@ -1046,14 +841,6 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-let level_subst_of f = 
-  fun l -> 
-    try let u = f l in 
-	  match Universe.level u with
-	  | None -> l
-	  | Some l -> l
-    with Not_found -> l
-     
 module Instance : sig 
     type t = Level.t array
 
@@ -1062,68 +849,27 @@ module Instance : sig
     val equal : t -> t -> bool
     val subst_fn : universe_level_subst_fn -> t -> t
     val subst : universe_level_subst -> t -> t
-    val pr : t -> Pp.std_ppcmds
-    val check_eq : t check_function 
+    val pr : t -> Pp.t
+    val check_eq : t check_function
+    val length : t -> int
+    val append : t -> t -> t
+    val of_array : Level.t array -> t
 end = 
 struct
   type t = Level.t array
 
-  let empty : t = [||]
-
-  module HInstancestruct =
-  struct
-    type _t = t
-    type t = _t
-    type u = Level.t -> Level.t
-
-    let hashcons huniv a = 
-      let len = Array.length a in
-	if Int.equal len 0 then empty
-	else begin
-	  for i = 0 to len - 1 do
-	    let x = Array.unsafe_get a i in
-	    let x' = huniv x in
-	      if x == x' then ()
-	      else Array.unsafe_set a i x'
-	  done;
-	  a
-	end
-
-    let eq t1 t2 =
-      t1 == t2 ||
-	(Int.equal (Array.length t1) (Array.length t2) &&
-	   let rec aux i =
-	     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-	   in aux 0)
-	
-    let hash a = 
-      let accu = ref 0 in
-	for i = 0 to Array.length a - 1 do
-	  let l = Array.unsafe_get a i in
-	  let h = Level.hash l in
-	    accu := Hashset.Combine.combine !accu h;
-	done;
-	(* [h] must be positive. *)
-	let h = !accu land 0x3FFFFFFF in
-	  h
-  end
-
-  module HInstance = Hashcons.Make(HInstancestruct)
-
-  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
-    
-  let empty = hcons [||]
+  let empty = [||]
 
   let is_empty x = Int.equal (Array.length x) 0
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else hcons t'
+      if t' == t then t else t'
 
   let subst s t =
     let t' = 
       CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
-    in if t' == t then t else hcons t'
+    in if t' == t then t else t'
 
   let pr =
     prvect_with_sep spc Level.pr
@@ -1142,8 +888,41 @@ struct
 	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
 	 in aux 0)
 
+  let length = Array.length
+
+  let append = Array.append
+
+  let of_array i = i
+
 end
 
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1159,10 +938,80 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+  let size (univs, _) = Instance.length univs
+
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 end
 
 type universe_context = UContext.t
 
+module AUContext =
+struct
+  include UContext
+
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
+
+type abstract_universe_context = AUContext.t
+
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let check_subtype x y = match x, y with
+  | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+  | Irrelevant, Covariant -> false
+  | (Covariant | Invariant), Covariant -> true
+  | (Irrelevant | Covariant), Invariant -> false
+  | Invariant, Invariant -> true
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> Constraint.add (u, Le, u') csts
+    | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module CumulativityInfo =
+struct
+  type t = universe_context * Variance.t array
+
+  let univ_context (univcst, subtypcst) = univcst
+  let variance (univs, variance) = variance
+
+end
+
+module ACumulativityInfo = CumulativityInfo
+type abstract_cumulativity_info = ACumulativityInfo.t
+
 module ContextSet =
 struct
   type t = LSet.t constrained
@@ -1173,6 +1022,18 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+(** Instance subtyping *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = AUContext.repr ctx in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs inst in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
@@ -1192,43 +1053,9 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
-
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u csts
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1239,7 +1066,7 @@ let subst_univs_expr_opt fn (l,n) =
 
 let subst_univs_universe fn ul =
   let subst, nosubst = 
-    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+    List.fold_right (fun u (subst,nosubst) -> 
       try let a' = subst_univs_expr_opt fn u in
 	    (a' :: subst, nosubst)
       with Not_found -> (subst, u :: nosubst))
@@ -1250,7 +1077,7 @@ let subst_univs_universe fn ul =
       let substs = 
 	List.fold_left Universe.merge_univs Universe.empty subst
       in
-	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
+	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
 	  substs nosubst
 
 let merge_context strict ctx g =
@@ -1269,6 +1096,10 @@ let merge_context_set strict ctx g =
 
 (** Pretty-printing *)
 
+let pr_constraints prl = Constraint.pr prl
+    
+let pr_universe_context = UContext.pr
+
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()