From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Sep 2015 18:07:39 +0200
Subject: Universes: enforce Set <= i for all Type occurrences.

---
 kernel/indtypes.ml |  5 +++-
 kernel/univ.ml     | 71 ++++++++++++++++++++++++++++++++++--------------------
 kernel/univ.mli    | 10 +++++---
 3 files changed, 56 insertions(+), 30 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8c89abe940..9c065101a3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -286,7 +286,10 @@ let typecheck_inductive env mie =
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
 	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+				not (is_type0m_univ defu && not is_unit)
+				  (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
+
+			     )
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 336cdb653e..040e9bc270 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
   let is_small x = 
     match data x with
     | Level _ -> false
-    | _ -> true
-
+    | Var _ -> false
+    | Prop -> true
+    | Set -> true
+ 
   let is_prop x =
     match data x with
     | Prop -> true
@@ -670,7 +672,7 @@ let arc_is_lt arc = match arc.status with
 | Unset | SetLe -> false
 | SetLt -> true
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal ?(predicative=false) u = {univ=u; lt=[]; le=[]; rank=0; predicative; status = Unset}
 
 module UMap :
 sig
@@ -720,6 +722,16 @@ let enter_arc ca g =
 
 (* Every Level.t has a unique canonical arc representative *)
 
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+  {(terminal u) with lt=[v]}
+    
+let empty_universes =
+  let g = enter_arc (terminal ~predicative:true Level.set) UMap.empty in
+  let g = enter_arc (terminal_lt Level.prop Level.set) g in
+    g
+
 (* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
@@ -733,6 +745,22 @@ let rec repr g u =
     | Equiv v -> repr g v
     | Canonical arc -> arc
 
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
+
+let add_universe vlev ~predicative g = 
+  let v = terminal ~predicative vlev in
+  let arc =
+    let arc =
+      if predicative then get_set_arc g else get_prop_arc g
+    in
+      { arc with le=vlev::arc.le}
+  in
+  let g = enter_arc arc g in
+    enter_arc v g
+
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
@@ -745,6 +773,8 @@ let safe_repr g u =
   try g, safe_repr_rec g u
   with Not_found ->
     let can = terminal u in
+    let setarc = get_set_arc g in
+    let g = enter_arc {setarc with le=u::setarc.le} g in
     enter_arc can g, can
 
 (* reprleq : canonical_arc -> canonical_arc list *)
@@ -789,7 +819,6 @@ let between g arcu arcv =
   in
   let good,_,_ = explore ([arcv],[],false) arcu in
     good
-
 (* We assume  compare(u,v) = LE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
    Otherwise, between g u v = []
@@ -900,8 +929,9 @@ let get_explanation strict g arcu arcv =
         in
         find [] arc.lt
   in
+  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
   try
-    let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
     (** Reset all the touched arcs. *)
     let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
     List.rev c
@@ -972,7 +1002,6 @@ let fast_compare_neq strict g arcu arcv =
     else process_le c to_revert (arc :: lt_todo) le_todo lt le
 
   in
-
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
     (** Reset all the touched arcs. *)
@@ -1021,10 +1050,6 @@ let check_equal g u v =
 
 let check_eq_level g u v = u == v || check_equal g u v
 
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
 let check_smaller g strict u v =
   let g, arcu = safe_repr g u in
   let g, arcv = safe_repr g v in
@@ -1120,7 +1145,7 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if Level.is_small arc.univ || arc.rank >= max_rank
+      if arc.rank >= max_rank && not (Level.is_small best_arc.univ)
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
@@ -1150,7 +1175,7 @@ let merge g arcu arcv =
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g arc1 arc2 =
-  let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
     if not (Int.equal arc1.rank arc2.rank) then arcu, g
     else
@@ -1173,8 +1198,8 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
   let g,arcu = safe_repr g u in
@@ -1225,18 +1250,10 @@ let enforce_univ_lt u v g =
         let p = get_explanation false g arcv arcu  in
         error_inconsistency Lt u v p
 
-let empty_universes = UMap.empty
-
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
 
 let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g = 
-  let v = terminal vlev in
-  let proparc = get_prop_arc g in
-    enter_arc {proparc with le=vlev::proparc.le}
-      (enter_arc v g)
       
 (* Constraints and sets of constraints. *)    
 
@@ -1370,10 +1387,12 @@ let check_univ_leq u v =
 
 let enforce_leq u v c =
   let open Universe.Huniv in
+  let rec aux acc v =
   match v with
-  | Cons (v, _, Nil) ->
-    fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  | Cons (v, _, l) ->
+    aux (fold (fun u -> constraint_add_leq u v) u c) l
+  | Nil -> acc
+  in aux c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe61..76453cbb08 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
-
+		       
+  val is_prop : t -> bool
+  val is_set : t -> bool
+  (** Is it specifically Prop or Set *)
+		       
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -159,8 +163,8 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= Prop or Set. *)
+val add_universe : universe_level -> predicative:bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
-- 
cgit v1.2.3


From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 21 Sep 2015 11:55:32 +0200
Subject: Forcing i > Set for global universes (incomplete)

---
 kernel/environ.ml     | 39 +++++++++++++++++++++++++++------------
 kernel/environ.mli    |  4 ++--
 kernel/term_typing.ml |  8 ++++----
 kernel/univ.ml        | 26 ++++++++++++++------------
 kernel/univ.mli       |  4 ++--
 5 files changed, 49 insertions(+), 32 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 109e3830c2..c433c07898 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env =
 
 (* Universe constraints *)
 
-let add_constraints c env =
-  if Univ.Constraint.is_empty c then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+				     
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then env
+  else map_universes (Univ.merge_constraints c) env
 
 let check_constraints c env =
   Univ.check_constraints c env.env_stratification.env_universes
 
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = c } }
-
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+  let g = Array.fold_left (fun g v -> Univ.add_universe v strict g)
+			  g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  in
+    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+  let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g)
+			 (Univ.ContextSet.levels ctx) g
+  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = c } }
 
 (* Global constants *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4ad0327fc7..9f6ea522a7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83e566041f..e89b6ef8f7 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -100,11 +100,11 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
+	      
 let infer_declaration env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context uctx env in
+      let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,7 +115,7 @@ let infer_declaration env kn dcl =
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:true c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -135,7 +135,7 @@ let infer_declaration env kn dcl =
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 040e9bc270..b61b441d2e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -750,17 +750,6 @@ let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
-let add_universe vlev ~predicative g = 
-  let v = terminal ~predicative vlev in
-  let arc =
-    let arc =
-      if predicative then get_set_arc g else get_prop_arc g
-    in
-      { arc with le=vlev::arc.le}
-  in
-  let g = enter_arc arc g in
-    enter_arc v g
-
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
@@ -777,6 +766,18 @@ let safe_repr g u =
     let g = enter_arc {setarc with le=u::setarc.le} g in
     enter_arc can g, can
 
+let add_universe vlev strict g = 
+  let v = terminal ~predicative:true vlev in
+  let arc =
+    let arc = get_set_arc g in
+      if strict then
+	{ arc with lt=vlev::arc.lt}
+      else 
+	{ arc with le=vlev::arc.le}
+  in
+  let g = enter_arc arc g in
+    enter_arc v g
+
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -1145,7 +1146,8 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if arc.rank >= max_rank && not (Level.is_small best_arc.univ)
+      if Level.is_small arc.univ ||
+	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 76453cbb08..fe7fc1ab9f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop or Set. *)
-val add_universe : universe_level -> predicative:bool -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set. *)
+val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
-- 
cgit v1.2.3


From cc69a4697633e14fc00c9bd0858b38120645464b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:00:49 +0200
Subject: Univs: module constraints move to universe contexts as they might
 declare new universes (e.g. with).

---
 kernel/declarations.mli |  4 ++--
 kernel/environ.ml       | 11 ++++++----
 kernel/mod_typing.ml    | 35 +++++++++++++++----------------
 kernel/mod_typing.mli   |  2 +-
 kernel/safe_typing.ml   | 55 ++++++++++++++++++++++++++-----------------------
 5 files changed, 56 insertions(+), 51 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 561c66b422..7def963e73 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -246,8 +246,8 @@ and module_body =
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
-    (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    (** set of all universes constraints in the module  *)
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : Mod_subst.delta_resolver;
     mod_retroknowledge : Retroknowledge.action list }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c433c07898..429aba4f75 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -197,8 +197,10 @@ let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
 let add_universes strict ctx g =
-  let g = Array.fold_left (fun g v -> Univ.add_universe v strict g)
-			  g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  let g = Array.fold_left
+	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
+	    (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     Univ.merge_constraints (Univ.UContext.constraints ctx) g
 			   
@@ -206,8 +208,9 @@ let push_context ?(strict=false) ctx env =
   map_universes (add_universes strict ctx) env
 
 let add_universes_set strict ctx g =
-  let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g)
-			 (Univ.ContextSet.levels ctx) g
+  let g = Univ.LSet.fold
+	    (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    (Univ.ContextSet.levels ctx) g
   in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 4f20e5f62a..7da0958eaf 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
 open Mod_subst
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.constraints
+  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
 
 let rec mp_from_mexpr = function
   | MEident mp -> mp
@@ -52,7 +52,7 @@ let rec rebuild_mp mp l =
   | []-> mp
   | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
 
-let (+++) = Univ.Constraint.union
+let (+++) = Univ.ContextSet.union
 
 let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
   let lab,idl = match idl with
@@ -75,30 +75,30 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
       let env' = Environ.add_constraints ccst env' in
       let newus, cst = Univ.UContext.dest ctx in
+      let ctxs = Univ.ContextSet.of_context ctx in
       let env' = Environ.add_constraints cst env' in
-      let c',cst = match cb.const_body with
+      let c',ctx' = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j = Typeops.infer env' c in
 	  let typ = Typeops.type_of_constant_type env' cb.const_type in
 	  let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 	    j.uj_type typ in
-	  j.uj_val,cst' +++ cst
+	    j.uj_val, Univ.ContextSet.add_constraints cst' ctxs
 	| Def cs ->
 	  let cst' = Reduction.infer_conv env' (Environ.universes env') c
 	    (Mod_subst.force_constr cs) in
 	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
-	    if cb.const_polymorphic then cst' +++ cst
-	    else cst' +++ cst
+	    (* if cb.const_polymorphic then  *)Univ.ContextSet.add_constraints cst' ctxs
+	    (* else cst' +++ cst *)
 	  in
             c, cst
       in
       let def = Def (Mod_subst.from_val c') in
-      let ctx' = Univ.UContext.make (newus, cst) in
       let cb' =
 	{ cb with
 	  const_body = def;
 	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
-	  const_universes = ctx' }
+	  const_universes = Univ.ContextSet.to_context ctx' }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
@@ -145,8 +145,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
 	  begin
             try
               let mtb_old = module_type_of_module old in
-              Subtyping.check_subtypes env' mtb_mp1 mtb_old
-                +++ old.mod_constraints
+              Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
 	    with Failure _ -> error_incorrect_with_constraint lab
 	  end
 	| Algebraic (NoFunctor (MEident(mp'))) ->
@@ -194,7 +193,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       | Algebraic (NoFunctor (MEident mp0)) ->
 	let mpnew = rebuild_mp mp0 idl in
 	check_modpath_equiv env' mpnew mp;
-	before@(lab,spec)::after, equiv, Univ.Constraint.empty
+	before@(lab,spec)::after, equiv, Univ.ContextSet.empty
       | _ -> error_generative_module_expected lab
       end
   with
@@ -207,8 +206,8 @@ let check_with env mp (sign,alg,reso,cst) = function
   |WithDef(idl,c) ->
     let struc = destr_nofunctor sign in
     let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
-    let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
-    (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
+    let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
+    (NoFunctor struc'),alg',reso, cst+++cst'
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
@@ -238,7 +237,7 @@ let rec translate_mse env mpo inl = function
         let mtb = lookup_modtype mp1 env in
         mtb.mod_type, mtb.mod_delta
     in
-    sign,Some (MEident mp1),reso,Univ.Constraint.empty
+    sign,Some (MEident mp1),reso,Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
     translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
   |MEwith(me, with_decl) ->
@@ -256,7 +255,7 @@ and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let body = subst_signature subst fbody_b in
   let alg' = mkalg alg mp1 in
   let reso' = subst_codom_delta_resolver subst reso in
-  body,alg',reso', cst1 +++ cst2
+  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
 
 let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
   | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
@@ -301,7 +300,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     mk_mod mp impl sign None cst reso
   |Some (params_mte,inl) ->
     let res_mtb = translate_modtype env mp inl params_mte in
-    let auto_mtb = mk_modtype mp sign Univ.Constraint.empty reso in
+    let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
     let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
     let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
     { res_mtb with
@@ -309,7 +308,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
       mod_expr = impl;
       (** cst from module body typing, cst' from subtyping, 
           and constraints from module type. *)
-      mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints }
+      mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
@@ -324,7 +323,7 @@ let rec translate_mse_incl env mp inl = function
   |MEident mp1 ->
     let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr mb.mod_type in
-    sign,None,mb.mod_delta,Univ.Constraint.empty
+    sign,None,mb.mod_delta,Univ.ContextSet.empty
   |MEapply (fe,arg) ->
     let ftrans = translate_mse_incl env mp inl fe in
     translate_apply env inl ftrans arg (fun _ _ -> None)
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index b39e821254..80db12b0d3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -30,7 +30,7 @@ val translate_modtype :
 *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.constraints
+  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 55e767321b..9417aa0801 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -118,8 +118,8 @@ type safe_environment =
     revstruct : structure_body;
     modlabels : Label.Set.t;
     objlabels : Label.Set.t;
-    univ : Univ.constraints;
-    future_cst : Univ.constraints Future.computation list;
+    univ : Univ.ContextSet.t;
+    future_cst : Univ.ContextSet.t Future.computation list;
     engagement : engagement option;
     required : vodigest DPMap.t;
     loads : (module_path * module_body) list;
@@ -148,7 +148,7 @@ let empty_environment =
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
     future_cst = [];
-    univ = Univ.Constraint.empty;
+    univ = Univ.ContextSet.empty;
     engagement = None;
     required = DPMap.empty;
     loads = [];
@@ -221,7 +221,7 @@ let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 type constraints_addition =
-  Now of Univ.constraints | Later of Univ.constraints Future.computation
+  Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation
 
 let add_constraints cst senv =
   match cst with
@@ -229,14 +229,14 @@ let add_constraints cst senv =
     {senv with future_cst = fc :: senv.future_cst}
   | Now cst ->
   { senv with
-    env = Environ.add_constraints cst senv.env;
-    univ = Univ.Constraint.union cst senv.univ }
+    env = Environ.push_context_set ~strict:true cst senv.env;
+    univ = Univ.ContextSet.union cst senv.univ }
 
 let add_constraints_list cst senv =
   List.fold_right add_constraints cst senv
 
-let push_context_set ctx = add_constraints (Now (Univ.ContextSet.constraints ctx))
-let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
+let push_context_set ctx = add_constraints (Now ctx)
+let push_context ctx = add_constraints (Now (Univ.ContextSet.of_context ctx))
 
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
@@ -373,9 +373,9 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   if cb.const_polymorphic then
-    [Now Univ.Constraint.empty]
+    [Now Univ.ContextSet.empty]
   else
-    let cstrs = Univ.UContext.constraints cb.const_universes in
+    let cstrs = Univ.ContextSet.of_context cb.const_universes in
       Now cstrs ::  
 	(match cb.const_body with
 	| (Undef _ | Def _) -> []
@@ -384,16 +384,14 @@ let globalize_constant_universes env cb =
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later (Future.chain
-                 ~greedy:(not (Future.is_exn fc))
-                 ~pure:true fc Univ.ContextSet.constraints)]
-            | Some c -> [Now (Univ.ContextSet.constraints c)])
+            | None -> [Later fc]
+            | Some c -> [Now c])
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
-    [Now Univ.Constraint.empty]
+    [Now Univ.ContextSet.empty]
   else
-    [Now (Univ.UContext.constraints mb.mind_universes)]
+    [Now (Univ.ContextSet.of_context mb.mind_universes)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
@@ -617,8 +615,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
     modlabels = Label.Set.add (fst newdef) oldsenv.modlabels;
     univ =
       List.fold_left (fun acc cst ->
-        Univ.Constraint.union acc (Future.force cst))
-      (Univ.Constraint.union senv.univ oldsenv.univ)
+        Univ.ContextSet.union acc (Future.force cst))
+      (Univ.ContextSet.union senv.univ oldsenv.univ)
       now_cst;
     future_cst = later_cst @ oldsenv.future_cst;
     (* engagement is propagated to the upper level *)
@@ -641,8 +639,8 @@ let end_module l restype senv =
   let senv'=
     propagate_loads { senv with
       env = newenv;
-      univ = Univ.Constraint.union senv.univ mb.mod_constraints} in
-  let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
+      univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
+  let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
   let newenv = Modops.add_module mb newenv in
   let newresolver =
     if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -667,7 +665,7 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
-  let newenv = Environ.add_constraints senv.univ newenv in
+  let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = propagate_loads {senv with env=newenv} in
   let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
@@ -696,7 +694,8 @@ let add_include me is_module inl senv =
     match sign with
     | MoreFunctor(mbid,mtb,str) ->
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
-      let senv = add_constraints (Now cst_sub) senv in
+      let senv = add_constraints
+		   (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) senv in
       let mpsup_delta =
 	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
       in
@@ -707,7 +706,7 @@ let add_include me is_module inl senv =
   in
   let resolver,sign,senv =
     let struc = NoFunctor (List.rev senv.revstruct) in
-    let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
+    let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
     compute_sign sign mtb resolver senv
   in
   let str = match sign with
@@ -801,8 +800,10 @@ let import lib cst vodigest senv =
   check_engagement senv.env lib.comp_enga;
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
-  let env = Environ.add_constraints mb.mod_constraints senv.env in
-  let env = Environ.push_context_set cst env in
+  let env = Environ.push_context_set ~strict:true
+				     (Univ.ContextSet.union mb.mod_constraints cst)
+				     senv.env
+  in
   mp,
   { senv with
     env =
@@ -855,7 +856,9 @@ let register_inline kn senv =
   let env = { env with env_globals = new_globals } in
   { senv with env = env_of_pre_env env }
 
-let add_constraints c = add_constraints (Now c)
+let add_constraints c =
+  add_constraints
+    (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
 
 
 (* NB: The next old comment probably refers to [propagate_loads] above.
-- 
cgit v1.2.3


From e841deb4750d43ab19f91907476d75fc73860c5a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:09:14 +0200
Subject: Univs (kernel) adapt to new invariants

Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
---
 kernel/univ.ml  | 84 +++++++++++++++++++--------------------------------------
 kernel/univ.mli |  6 ++++-
 2 files changed, 32 insertions(+), 58 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index b61b441d2e..782778d09f 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -657,7 +657,6 @@ type canonical_arc =
       lt: Level.t list;
       le: Level.t list;
       rank : int;
-      predicative : bool;
       mutable status : status;
       (** Guaranteed to be unset out of the [compare_neq] functions. It is used
           to do an imperative traversal of the graph, ensuring a O(1) check that
@@ -672,7 +671,7 @@ let arc_is_lt arc = match arc.status with
 | Unset | SetLe -> false
 | SetLt -> true
 
-let terminal ?(predicative=false) u = {univ=u; lt=[]; le=[]; rank=0; predicative; status = Unset}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
 
 module UMap :
 sig
@@ -728,7 +727,7 @@ let terminal_lt u v =
   {(terminal u) with lt=[v]}
     
 let empty_universes =
-  let g = enter_arc (terminal ~predicative:true Level.set) UMap.empty in
+  let g = enter_arc (terminal Level.set) UMap.empty in
   let g = enter_arc (terminal_lt Level.prop Level.set) g in
     g
 
@@ -750,33 +749,23 @@ let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
-
-let safe_repr g u =
-  let rec safe_repr_rec g u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec g v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec g u
-  with Not_found ->
-    let can = terminal u in
-    let setarc = get_set_arc g in
-    let g = enter_arc {setarc with le=u::setarc.le} g in
-    enter_arc can g, can
-
-let add_universe vlev strict g = 
-  let v = terminal ~predicative:true vlev in
-  let arc =
-    let arc = get_set_arc g in
-      if strict then
-	{ arc with lt=vlev::arc.lt}
-      else 
-	{ arc with le=vlev::arc.le}
-  in
-  let g = enter_arc arc g in
-    enter_arc v g
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
 
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
@@ -1045,20 +1034,18 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
-  arcu == arcv
+  let arcu = repr g u and arcv = repr g v in
+    arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
 
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
     is_prop_arc arcu 
-    || (is_set_arc arcu && arcv.predicative) 
+    || (is_set_arc arcu && not (is_prop_arc arcv))
     || is_leq g arcu arcv
 
 (** Then, checks on universes *)
@@ -1100,19 +1087,11 @@ let check_leq g u v =
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(** To speed up tests of Set </<= i *)
-let set_predicative g arcv = 
-  enter_arc {arcv with predicative = true} g
-
 (* setlt : Level.t -> Level.t -> reason -> unit *)
 (* forces u > v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setlt g arcu arcv =
   let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
-  let g = 
-    if is_set_arc arcu then set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1126,11 +1105,6 @@ let setlt_if (g,arcu) v =
 (* this is normally an update of u in g rather than a creation. *)
 let setleq g arcu arcv =
   let arcu' = {arcu with le=arcv.univ::arcu.le} in
-  let g = 
-    if is_set_arc arcu' then
-      set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1204,8 +1178,7 @@ let error_inconsistency o u v (p:explanation option) =
 (* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT ->
@@ -1224,8 +1197,7 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -1238,8 +1210,7 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -1465,7 +1436,6 @@ let normalize_universes g =
         lt = LSet.elements lt;
         le = LSet.elements le;
 	rank = rank;
-	predicative = false;
 	status = Unset;
       }
   in
@@ -1610,7 +1580,7 @@ let sort_universes orig =
   let fold i accu u =
     if 0 < i then
       let pred = types.(i - 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
       UMap.add u (Canonical arc) accu
     else accu
   in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index fe7fc1ab9f..ad33d597ea 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,7 +163,11 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= or > Set. *)
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
 val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)
-- 
cgit v1.2.3


From 0bc47a571c050979921bffd0b790a24a75ad990e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 15:14:58 +0200
Subject: Univs: handle side-effects of futures correctly in kernel.

---
 kernel/safe_typing.ml |  2 +-
 kernel/term_typing.ml | 40 +++++++++++++++++++++++++---------------
 2 files changed, 26 insertions(+), 16 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9417aa0801..43358d604d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -233,7 +233,7 @@ let add_constraints cst senv =
     univ = Univ.ContextSet.union cst senv.univ }
 
 let add_constraints_list cst senv =
-  List.fold_right add_constraints cst senv
+  List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
 let push_context_set ctx = add_constraints (Now ctx)
 let push_context ctx = add_constraints (Now (Univ.ContextSet.of_context ctx))
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e89b6ef8f7..926b387942 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -45,8 +45,8 @@ let map_option_typ = function None -> `None | Some x -> `Some x
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
 
-let handle_side_effects env body side_eff =
-  let handle_sideff t se =
+let handle_side_effects env body ctx side_eff =
+  let handle_sideff (t,ctx) se =
     let cbl = match se with
       | SEsubproof (c,cb,b) -> [c,cb,b]
       | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -66,7 +66,7 @@ let handle_side_effects env body side_eff =
       | Const (c',u') when eq_constant c c' -> 
 	Vars.subst_instance_constr u' b
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
-    let fix_body (c,cb,b) t =
+    let fix_body (c,cb,b) (t,ctx) =
       match cb.const_body, b with
       | Def b, _ ->
           let b = Mod_subst.force_constr b in
@@ -74,25 +74,29 @@ let handle_side_effects env body side_eff =
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkLetIn (cname c, b, b_ty, t)
+	        mkLetIn (cname c, b, b_ty, t),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else 
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | OpaqueDef _, `Opaque (b,_) -> 
 	  let poly = cb.const_polymorphic in
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
+	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)		
 	    else
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | _ -> assert false
     in
-      List.fold_right fix_body cbl t
+      List.fold_right fix_body cbl (t,ctx)
   in
   (* CAVEAT: we assure a proper order *)
-  Declareops.fold_side_effects handle_sideff body
+  Declareops.fold_side_effects handle_sideff (body,ctx)
     (Declareops.uniquize_side_effects side_eff)
 
 let hcons_j j =
@@ -120,7 +124,7 @@ let infer_declaration env kn dcl =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body = handle_side_effects env body side_eff in
+          let body,ctx = handle_side_effects env body ctx side_eff in
 	  let env' = push_context_set ctx env in
           let j = infer env' body in
           let j = hcons_j j in
@@ -135,14 +139,16 @@ let infer_declaration env kn dcl =
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      assert(Univ.ContextSet.is_empty ctx);
-      let body = handle_side_effects env body side_eff in
+      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+      let body, ctx = handle_side_effects env body
+        (Univ.ContextSet.union univsctx ctx) side_eff in
+      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
-      let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
+      let usubst, univs =
+	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
       let j = infer env body in
       let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
@@ -306,5 +312,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 let handle_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
+			 let body, ctx' = handle_side_effects env body ctx side_eff in
+			 (body, ctx'), Declareops.no_seff);
 }
+
+let handle_side_effects env body side_eff =
+  fst (handle_side_effects env body Univ.ContextSet.empty side_eff)
-- 
cgit v1.2.3


From 0adf0838a59a3fbca1ced05243ccc42c969fcf18 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 17:49:33 +0200
Subject: Univs: uncovered bug in strengthening of opaque polymorphic
 definitions.

---
 kernel/modops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index d52fe611c0..8733ca8c2f 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -331,8 +331,10 @@ let strengthen_const mp_from l cb resolver =
     let kn = KerName.make2 mp_from l in
     let con = constant_of_delta_kn resolver kn in
     let u = 
-      if cb.const_polymorphic then 
-	Univ.UContext.instance cb.const_universes
+      if cb.const_polymorphic then
+	let u = Univ.UContext.instance cb.const_universes in
+	let s = Univ.make_instance_subst u in
+	  Univ.subst_univs_level_instance s u
       else Univ.Instance.empty
     in
       { cb with
-- 
cgit v1.2.3


From e5cbf1ef44449f60eec3bb3c52d08b2943283279 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:30:44 +0200
Subject: Univs: fix subtyping of polymorphic parameters.

---
 kernel/subtyping.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index db155e6c86..463e28a1c6 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -311,9 +311,12 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		try 
 		  (* The environment with the expected universes plus equality 
 		     of the body instances with the expected instance *)
-		  let env = Environ.add_constraints cstrs env in
-		    (* Check that the given definition does not add any constraint over
-		       the expected ones, so that it can be used in place of the original. *)
+		  let ctxi = Univ.Instance.append inst1 inst2 in
+		  let ctx = Univ.UContext.make (ctxi, cstrs) in
+		  let env = Environ.push_context ctx env in
+		  (* Check that the given definition does not add any constraint over
+		     the expected ones, so that it can be used in place of 
+                     the original. *)
 		    if Univ.check_constraints ctx1 (Environ.universes env) then
 		      cstrs, env, inst2
 		    else error (IncompatibleConstraints ctx1)
-- 
cgit v1.2.3


From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:36:57 +0200
Subject: Univs: fix bug #4251, handling of template polymorphic constants.

---
 kernel/inductive.ml | 5 ++++-
 kernel/univ.ml      | 4 ++++
 kernel/univ.mli     | 3 +++
 3 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 87c139f48d..a02d5e2055 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,7 +165,10 @@ let rec make_subst env =
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-        make (cons_subst u s subst) (sign, exp, args)
+	  if Univ.Universe.is_levels s then
+            make (cons_subst u s subst) (sign, exp, args)
+	  else (* Cannot handle substitution by i+n universes. *)
+	    make subst (sign, exp, args)
     | (na,None,t)::sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 782778d09f..73d323426b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -553,6 +553,10 @@ struct
     | Cons (l, _, Nil) -> Expr.is_level l
     | _ -> false
 
+  let rec is_levels l = match l with
+    | Cons (l, _, r) -> Expr.is_level l && is_levels r
+    | Nil -> true
+
   let level l = match l with
     | Cons (l, _, Nil) -> Expr.level l
     | _ -> None
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ad33d597ea..4cc8a2528f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -91,6 +91,9 @@ sig
   val is_level : t -> bool
   (** Test if the universe is a level or an algebraic universe. *)
 
+  val is_levels : t -> bool
+  (** Test if the universe is a lub of levels or contains +n's. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
-- 
cgit v1.2.3


From d4869e059bfb73d99e1f5ef1b0a1f0906fa27056 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:40:17 +0200
Subject: Univs: correct handling of with in modules

For polymorphic and non-polymorphic parameters and definitions, fixes
bugs #4298, #4294
---
 kernel/mod_typing.ml | 73 +++++++++++++++++++++++++++++++++++++---------------
 kernel/subtyping.ml  |  4 ++-
 2 files changed, 55 insertions(+), 22 deletions(-)

(limited to 'kernel')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7da0958eaf..3be89afbde 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,33 +72,64 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
-      let env' = Environ.add_constraints ccst env' in
-      let newus, cst = Univ.UContext.dest ctx in
-      let ctxs = Univ.ContextSet.of_context ctx in
-      let env' = Environ.add_constraints cst env' in
-      let c',ctx' = match cb.const_body with
-	| Undef _ | OpaqueDef _ ->
-	  let j = Typeops.infer env' c in
-	  let typ = Typeops.type_of_constant_type env' cb.const_type in
-	  let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-	    j.uj_type typ in
-	    j.uj_val, Univ.ContextSet.add_constraints cst' ctxs
-	| Def cs ->
-	  let cst' = Reduction.infer_conv env' (Environ.universes env') c
-	    (Mod_subst.force_constr cs) in
-	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
-	    (* if cb.const_polymorphic then  *)Univ.ContextSet.add_constraints cst' ctxs
-	    (* else cst' +++ cst *)
+      let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
+      let uctx = (* Context of the spec *)
+	if cb.const_polymorphic then
+	  Univ.instantiate_univ_context uctx
+	else uctx
+      in
+      let c', univs, ctx' = 
+	if not cb.const_polymorphic then
+	  let env' = Environ.push_context ~strict:true uctx env' in
+	  let env' = Environ.push_context ~strict:true ctx env' in
+	  let c',cst = match cb.const_body with
+	    | Undef _ | OpaqueDef _ ->
+	      let j = Typeops.infer env' c in
+	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+						j.uj_type typ in
+	      j.uj_val, cst'
+	    | Def cs ->
+	       let c' = Mod_subst.force_constr cs in
+	         c, Reduction.infer_conv env' (Environ.universes env') c c'
+	  in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+	else
+	  let cus, ccst = Univ.UContext.dest uctx in
+	  let newus, cst = Univ.UContext.dest ctx in
+	  let () =
+	    if not (Univ.Instance.length cus == Univ.Instance.length newus) then
+	      error_incorrect_with_constraint lab
+	  in
+	  let inst = Univ.Instance.append cus newus in
+	  let csti = Univ.enforce_eq_instances cus newus cst in
+	  let csta = Univ.Constraint.union csti ccst in
+	  let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
+	  let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+		     error_incorrect_with_constraint lab
+	  in
+	  let cst = match cb.const_body with
+	    | Undef _ | OpaqueDef _ ->
+	      let j = Typeops.infer env' c in
+	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+						j.uj_type typ in
+	      cst'
+	    | Def cs ->
+	       let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+	        cst'
 	  in
-            c, cst
+	    if not (Univ.Constraint.is_empty cst) then
+	      error_incorrect_with_constraint lab;
+	    let subst, ctx = Univ.abstract_universes true ctx in
+	      Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
-	  const_universes = Univ.ContextSet.to_context ctx' }
+	  const_universes = univs;
+	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 463e28a1c6..58f3bcdf00 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -322,7 +322,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
 		  error (IncompatibleUniverses incon)
-	else cst, env, Univ.Instance.empty
+	else
+	  cst, env, Univ.Instance.empty
       in
       (* Now check types *)
       let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -459,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   let env = add_module_type sup.mod_mp sup env in
+  let env = Environ.push_context_set ~strict:true super.mod_constraints env in
   check_modtypes Univ.Constraint.empty env
     (strengthen sup sup.mod_mp) super empty_subst
     (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
-- 
cgit v1.2.3


From 1d01533266b247cbc32903935963674acf7c6c54 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:05:48 +0200
Subject: Univs: forgot a substitution in mod_typing.

---
 kernel/mod_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3be89afbde..922652287b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -111,6 +111,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
 	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = Vars.subst_instance_constr cus typ in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
-- 
cgit v1.2.3


From 4585baa53e7fa4c25e304b8136944748a7622e10 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 18:42:38 +0200
Subject: Univs: refined handling of assumptions

According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
---
 kernel/safe_typing.ml  | 51 ++++++++++++++++++++++++++------------------------
 kernel/safe_typing.mli |  7 ++++---
 2 files changed, 31 insertions(+), 27 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 43358d604d..4299f729da 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -221,22 +221,23 @@ let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 type constraints_addition =
-  Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation
+  | Now of bool * Univ.ContextSet.t
+  | Later of Univ.ContextSet.t Future.computation
 
 let add_constraints cst senv =
   match cst with
   | Later fc -> 
     {senv with future_cst = fc :: senv.future_cst}
-  | Now cst ->
+  | Now (poly,cst) ->
   { senv with
-    env = Environ.push_context_set ~strict:true cst senv.env;
+    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
     univ = Univ.ContextSet.union cst senv.univ }
 
 let add_constraints_list cst senv =
   List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
-let push_context_set ctx = add_constraints (Now ctx)
-let push_context ctx = add_constraints (Now (Univ.ContextSet.of_context ctx))
+let push_context_set poly ctx = add_constraints (Now (poly,ctx))
+let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
 
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
@@ -246,7 +247,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
   List.fold_left
     (fun e fc ->
        if Future.UUIDSet.mem (Future.uuid fc) except then e
-       else add_constraints (Now (Future.join fc)) e)
+       else add_constraints (Now (false, Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
 let is_joined_environment e = List.is_empty e.future_cst 
@@ -337,20 +338,20 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let senv' = push_context univs senv in
+  let senv' = push_context de.Entries.const_entry_polymorphic univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
     | OpaqueDef o ->
         Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
-        push_context_set
-          (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
+        push_context_set de.Entries.const_entry_polymorphic
+	 (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
           senv'
     | _ -> assert false in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ((id,t),ctx) senv =
-  let senv' = push_context_set ctx senv in
+let push_named_assum ((id,t,poly),ctx) senv =
+  let senv' = push_context_set poly ctx senv in
   let t = Term_typing.translate_local_assum senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
@@ -373,10 +374,10 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   if cb.const_polymorphic then
-    [Now Univ.ContextSet.empty]
+    [Now (true, Univ.ContextSet.empty)]
   else
     let cstrs = Univ.ContextSet.of_context cb.const_universes in
-      Now cstrs ::  
+      Now (false, cstrs) ::  
 	(match cb.const_body with
 	| (Undef _ | Def _) -> []
 	| OpaqueDef lc ->
@@ -385,20 +386,20 @@ let globalize_constant_universes env cb =
 	  | Some fc ->
             match Future.peek_val fc with
             | None -> [Later fc]
-            | Some c -> [Now c])
+            | Some c -> [Now (false, c)])
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
-    [Now Univ.ContextSet.empty]
+    [Now (true, Univ.ContextSet.empty)]
   else
-    [Now (Univ.ContextSet.of_context mb.mind_universes)]
+    [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
   | SFBconst cb -> globalize_constant_universes env cb
   | SFBmind mib -> globalize_mind_universes mib
-  | SFBmodtype mtb -> [Now mtb.mod_constraints]
-  | SFBmodule mb -> [Now mb.mod_constraints]
+  | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
+  | SFBmodule mb -> [Now (false, mb.mod_constraints)]
 
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
@@ -501,13 +502,13 @@ let add_modtype l params_mte inl senv =
 (** full_add_module adds module with universes and constraints *)
 
 let full_add_module mb senv =
-  let senv = add_constraints (Now mb.mod_constraints) senv in
+  let senv = add_constraints (Now (false, mb.mod_constraints)) senv in
   let dp = ModPath.dp mb.mod_mp in
   let linkinfo = Nativecode.link_info_of_dirpath dp in
   { senv with env = Modops.add_linked_module mb linkinfo senv.env }
 
 let full_add_module_type mp mt senv =
-  let senv = add_constraints (Now mt.mod_constraints) senv in
+  let senv = add_constraints (Now (false, mt.mod_constraints)) senv in
   { senv with env = Modops.add_module_type mp mt senv.env }
 
 (** Insertion of modules *)
@@ -688,14 +689,16 @@ let add_include me is_module inl senv =
       let mtb = translate_modtype senv.env mp_sup inl ([],me) in
       mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
   in
-  let senv = add_constraints (Now cst) senv in
+  let senv = add_constraints (Now (false, cst)) senv in
   (* Include Self support  *)
   let rec compute_sign sign mb resolver senv =
     match sign with
     | MoreFunctor(mbid,mtb,str) ->
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
-      let senv = add_constraints
-		   (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) senv in
+      let senv =
+	add_constraints
+	  (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
+	  senv in
       let mpsup_delta =
 	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
       in
@@ -858,7 +861,7 @@ let register_inline kn senv =
 
 let add_constraints c =
   add_constraints
-    (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
+    (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
 
 
 (* NB: The next old comment probably refers to [propagate_loads] above.
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2b4324b96f..b971a1bd42 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,7 +57,8 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
+  (Id.t * Term.types * bool (* polymorphic *))
+    Univ.in_universe_context_set -> safe_transformer0
 val push_named_def :
   Id.t * Entries.definition_entry -> safe_transformer0
 
@@ -88,10 +89,10 @@ val add_modtype :
 (** Adding universe constraints *)
 
 val push_context_set :
-  Univ.universe_context_set -> safe_transformer0
+  bool -> Univ.universe_context_set -> safe_transformer0
 
 val push_context :
-  Univ.universe_context -> safe_transformer0
+  bool -> Univ.universe_context -> safe_transformer0
 
 val add_constraints :
   Univ.constraints -> safe_transformer0
-- 
cgit v1.2.3


From 8860362de4a26286b0cb20cf4e02edc5209bdbd1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 23:35:51 +0200
Subject: Univs: Change intf of push_named_def to return the computed universe
 context

Let-bound definitions can be opaque but the whole universe context
was not gathered to be discharged at section closing time.
---
 kernel/safe_typing.ml  | 17 +++++++++--------
 kernel/safe_typing.mli |  5 ++++-
 2 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4299f729da..9329b16861 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -338,17 +338,18 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let senv' = push_context de.Entries.const_entry_polymorphic univs senv in
-  let c, senv' = match c with
-    | Def c -> Mod_subst.force_constr c, senv'
+  let poly = de.Entries.const_entry_polymorphic in
+  let univs = Univ.ContextSet.of_context univs in
+  let c, univs = match c with
+    | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
-        Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
-        push_context_set de.Entries.const_entry_polymorphic
-	 (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
-          senv'
+        Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
+        Univ.ContextSet.union univs 
+	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
     | _ -> assert false in
+  let senv' = push_context_set poly univs senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
-    {senv' with env=env''}
+    univs, {senv' with env=env''}
 
 let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b971a1bd42..eac08eb834 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -59,8 +59,11 @@ val is_joined_environment : safe_environment -> bool
 val push_named_assum :
   (Id.t * Term.types * bool (* polymorphic *))
     Univ.in_universe_context_set -> safe_transformer0
+
+(** Returns the full universe context necessary to typecheck the definition
+  (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.definition_entry -> safe_transformer0
+  Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
-- 
cgit v1.2.3