- Fix bug preventing apply from unfolding Fixpoints.

- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v

15 files changed, 200 insertions, 113 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 4363ec442..55868097f 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -47,12 +47,14 @@ let constraints_of_constant cb = Univ.Constraint.union
   (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o))
+  | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o))
 
 let universes_of_constant cb = 
   match cb.const_body with
   | Undef _ | Def _ -> cb.const_universes
-  | OpaqueDef o -> Opaqueproof.force_constraints o
+  | OpaqueDef o -> 
+    Univ.UContext.union cb.const_universes 
+      (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
 
 let universes_of_polymorphic_constant cb = 
   if cb.const_polymorphic then universes_of_constant cb
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 001a1e4b3..07c18d5e3 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_private : bool option }
 
 (** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr * Declareops.side_effects
+type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
 type const_entry_body = proof_output Future.computation
 
 type projection = mutual_inductive * int * int * types
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd4237b22..7a90f3675 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -311,17 +311,21 @@ let evaluable_constant kn env =
     | OpaqueDef _ -> false
     | Undef _ -> false
 
-let template_polymorphic_constant (cst,u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else
-    match (lookup_constant cst env).const_type with 
-    | TemplateArity _ -> true
-    | RegularArity _ -> false
+let polymorphic_constant cst env =
+  (lookup_constant cst env).const_polymorphic
 
-let polymorphic_constant (cst,u) env =
+let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
-  else
-    (lookup_constant cst env).const_polymorphic
+  else polymorphic_constant cst env
+
+let template_polymorphic_constant cst env =
+  match (lookup_constant cst env).const_type with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pconstant (cst,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_constant cst env
 
 let lookup_projection cst env =
   match (lookup_constant cst env).const_proj with 
@@ -336,17 +340,21 @@ let is_projection cst env =
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
 
-let template_polymorphic_ind ((mind,i),u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else
-    match (lookup_mind mind env).mind_packets.(i).mind_arity with 
-    | TemplateArity _ -> true
-    | RegularArity _ -> false
+let polymorphic_ind (mind,i) env =
+  (lookup_mind mind env).mind_polymorphic
 
-let polymorphic_ind ((mind,i),u) env =
+let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
-  else
-    (lookup_mind mind env).mind_polymorphic
+  else polymorphic_ind ind env
+
+let template_polymorphic_ind (mind,i) env =
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pind (ind,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_ind ind env
   
 let add_mind_key kn mind_key env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 28eecc7ef..61a4f7327 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -128,10 +128,12 @@ val lookup_constant    : constant -> env -> constant_body
 val evaluable_constant : constant -> env -> bool
 
 (** New-style polymorphism *)
-val polymorphic_constant : pconstant -> env -> bool
+val polymorphic_constant  : constant -> env -> bool
+val polymorphic_pconstant : pconstant -> env -> bool
 
 (** Old-style polymorphism *)
-val template_polymorphic_constant : pconstant -> env -> bool
+val template_polymorphic_constant  : constant -> env -> bool
+val template_polymorphic_pconstant : pconstant -> env -> bool
 
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
@@ -173,10 +175,12 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
 (** New-style polymorphism *)
-val polymorphic_ind : pinductive -> env -> bool
+val polymorphic_ind  : inductive -> env -> bool
+val polymorphic_pind : pinductive -> env -> bool
 
 (** Old-style polymorphism *)
-val template_polymorphic_ind : pinductive -> env -> bool
+val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_pind : pinductive -> env -> bool
 
 (** {5 Modules } *)
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index bb5695885..6d48aaa4e 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -384,11 +384,11 @@ let rec execute env cstr =
         let argst = execute_array env args in
 	let ft =
 	  match kind_of_term f with
-	  | Ind ind when Environ.template_polymorphic_ind ind env ->
+	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	      (* Template sort-polymorphism of inductive types *)
 	    let args = Array.map (fun t -> lazy t) argst in
 	      judge_of_inductive_knowing_parameters env ind args
-	  | Const cst when Environ.template_polymorphic_constant cst env ->
+	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
 	      (* Template sort-polymorphism of constants *)
 	    let args = Array.map (fun t -> lazy t) argst in
 	      judge_of_constant_knowing_parameters env cst args
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 73fdaa81f..0f9c7421f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -193,6 +193,34 @@ let cumulate_arity_large_levels env sign =
 let is_impredicative env u =
   is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
 
+let param_ccls params =
+  let has_some_univ u = function
+    | Some v when Universe.equal u v -> true
+    | _ -> false
+  in
+  let remove_some_univ u = function
+    | Some v when Universe.equal u v -> None
+    | x -> x
+  in
+  let fold l (_, b, p) = match b with
+  | None ->
+    (* Parameter contributes to polymorphism only if explicit Type *)
+    let c = strip_prod_assum p in
+    (* Add Type levels to the ordered list of parameters contributing to *)
+    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
+    begin match kind_of_term c with
+    | Sort (Type u) ->
+      if List.exists (has_some_univ u) l then
+        None :: List.map (remove_some_univ u) l
+      else
+        Some u :: l
+    | _ ->
+      None :: l
+    end
+  | _ -> l
+  in
+    List.fold_left fold [] params
+
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
 (* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -215,7 +243,7 @@ let typecheck_inductive env ctx mie =
     List.fold_left
       (fun (env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-         let arity = 
+         let arity, expltype = 
 	   if isArity ind.mind_entry_arity then
 	     let (ctx,s) = destArity ind.mind_entry_arity in
 	       match s with
@@ -226,11 +254,12 @@ let typecheck_inductive env ctx mie =
 	         let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
 		 let (cctx, _) = destArity proparity.utj_val in
 		   (* Any universe is well-formed, we don't need to check [s] here *)
-		   mkArity (cctx, s)
-	       | _ -> let arity = infer_type env_params ind.mind_entry_arity in
-			arity.utj_val
+		   mkArity (cctx, s), not (Sorts.is_small s)
+	       | _ -> 
+		 let arity = infer_type env_params ind.mind_entry_arity in
+		   arity.utj_val, not (Sorts.is_small s)
 	   else let arity = infer_type env_params ind.mind_entry_arity in
-		  arity.utj_val
+		  arity.utj_val, false
 	 in
 	 let (sign, deflev) = dest_arity env_params arity in
 	 let inflev = 
@@ -249,7 +278,7 @@ let typecheck_inductive env ctx mie =
 	 let env_ar' =
            push_rel (Name id, None, full_arity) env_ar in
              (* (add_constraints cst2 env_ar) in *)
-	   (env_ar', (id,full_arity,sign @ params,deflev,inflev)::l))
+	   (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
       (env',[])
       mie.mind_entry_inds in
 
@@ -277,30 +306,60 @@ let typecheck_inductive env ctx mie =
   (* Compute/check the sorts of the inductive types *)
 
   let inds =
-    Array.map (fun ((id,full_arity,sign,def_level,inf_level),cn,lc,(is_unit,clev))  ->
-      let defu = Term.univ_of_sort def_level in
-      let infu = 
-	(** Inferred level, with parameters and constructors. *)
-	match inf_level with
-	| Some alev -> Universe.sup clev alev
-	| None -> clev
+    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev))  ->
+      let full_polymorphic () = 
+	let defu = Term.univ_of_sort def_level in
+	let infu = 
+	  (** Inferred level, with parameters and constructors. *)
+	  match inf_level with
+	  | Some alev -> Universe.sup clev alev
+	  | None -> clev
+	in
+	let is_natural =
+	  check_leq (universes env') infu defu && 
+	    not (is_type0m_univ defu && not is_unit)
+	in
+	let _ =
+	  (** Impredicative sort, always allow *)
+	  if is_impredicative env defu then ()
+	  else (** Predicative case: the inferred level must be lower or equal to the
+		   declared level. *)
+	    if not is_natural then
+	      anomaly ~label:"check_inductive" 
+		(Pp.str"Incorrect universe " ++
+		   Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
+		 ++ Universe.pr infu)
+	in
+	  RegularArity (not is_natural,full_arity,defu)
       in
-      let is_natural =
-	check_leq (universes env') infu defu && 
-	not (is_type0m_univ defu && not is_unit)
+      let template_polymorphic () =
+	let sign, s =
+          try dest_arity env full_arity
+          with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
+	in
+	  match s with
+	  | Type u when expltype (* Explicitly polymorphic *) ->
+	      (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *)
+	    (* The polymorphic level is a function of the level of the *)
+	    (* conclusions of the parameters *)
+            (* We enforce [u >= lev] in case [lev] has a strict upper *)
+            (* constraints over [u] *)
+	    let b = check_leq (universes env') clev u in
+	      if not b then
+		anomaly ~label:"check_inductive" 
+		  (Pp.str"Incorrect universe " ++
+		     Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
+		   ++ Universe.pr clev)
+	      else
+		TemplateArity (param_ccls params, clev)
+	  | _ (* Not an explicit occurrence of Type *) ->
+	    full_polymorphic ()
       in
-      let _ =
-	(** Impredicative sort, always allow *)
-	if is_impredicative env defu then ()
-	else (** Predicative case: the inferred level must be lower or equal to the
-		 declared level. *)
-	  if not is_natural then
-	    anomaly ~label:"check_inductive" 
-	    (Pp.str"Incorrect universe " ++
-	     Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
-	     ++ Universe.pr infu)
+      let arity = 
+	if mie.mind_entry_polymorphic then full_polymorphic ()
+	else template_polymorphic ()
       in
-	(id,cn,lc,(sign,RegularArity (not is_natural,full_arity,defu))))
+	(id,cn,lc,(sign,arity)))
     inds
   in (env_arities, params, inds)
 
@@ -617,7 +676,7 @@ let allowed_sorts is_smashed s =
 
 let arity_conclusion = function
   | RegularArity (_, c, _) -> c
-  | TemplateArity s -> mkType s.template_level
+  | TemplateArity (_, s) -> mkType s
 
 let fold_inductive_blocks f =
   Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
@@ -681,7 +740,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     (* Elimination sorts *)
     let arkind,kelim = 
       match ar_kind with
-      | TemplateArity ar -> TemplateArity ar, all_sorts
+      | TemplateArity (paramlevs, lev) -> 
+	let ar = {template_param_levels = paramlevs; template_level = lev} in
+	  TemplateArity ar, all_sorts
       | RegularArity (info,ar,defs) ->
 	let s = sort_of_univ defs in
 	let kelim = allowed_sorts info s in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 73d5c5db2..7aed4bf50 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 type cooking_info = { 
   modlist : work_list; 
   abstract : Context.named_context in_universe_context } 
-type proofterm = (constr * Univ.universe_context) Future.computation
+type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
@@ -99,7 +99,7 @@ let force_constraints = function
   | NoIndirect(_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       match !get_univ dp i with
-      | None -> Univ.UContext.empty
+      | None -> Univ.ContextSet.empty
       | Some u -> Future.force u
 
 let get_constraints = function
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index fee15e405..3e45f65b4 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -19,7 +19,7 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.universe_context) Future.computation
+type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque
 
 (** From a [proofterm] to some [opaque]. *)
@@ -31,9 +31,9 @@ val turn_indirect : opaque -> opaque
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
 val force_proof : opaque -> constr
-val force_constraints : opaque -> Univ.universe_context
+val force_constraints : opaque -> Univ.universe_context_set
 val get_proof : opaque -> Term.constr Future.computation
-val get_constraints : opaque -> Univ.universe_context Future.computation option
+val get_constraints : opaque -> Univ.universe_context_set Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -66,7 +66,7 @@ val set_indirect_creator :
 val set_indirect_opaque_accessor :
   (DirPath.t -> int -> Term.constr Future.computation) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.universe_context Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit
 val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
 val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
 val reset_indirect_creator : unit -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index deabf1bcf..960fb1f45 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -200,6 +200,9 @@ let add_constraints cst senv =
     env = Environ.add_constraints cst senv.env;
     univ = Univ.Constraint.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))
 
@@ -298,11 +301,12 @@ 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 c, univs = match c with
-    | Def c -> Mod_subst.force_constr c, univs
-    | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o
-    | _ -> assert false in
   let senv' = push_context univs senv in
+  let c, senv' = match c with
+    | Def c -> Mod_subst.force_constr c, senv' 
+    | OpaqueDef o -> Opaqueproof.force_proof o, 
+      push_context_set (Opaqueproof.force_constraints o) senv'
+    | _ -> assert false in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
@@ -330,30 +334,32 @@ let labels_of_mib mib =
 
 let globalize_constant_universes cb =
   if cb.const_polymorphic then
-    Now Univ.Constraint.empty
+    [Now Univ.Constraint.empty]
   else
-    match cb.const_body with
-    | (Undef _ | Def _) -> Now (Univ.UContext.constraints cb.const_universes)
-    | OpaqueDef lc ->
-      match Opaqueproof.get_constraints lc with
-      | None -> Now (Univ.UContext.constraints cb.const_universes)
-      | Some fc ->
-        match Future.peek_val fc with
-        | None -> Later (Future.chain ~pure:true fc Univ.UContext.constraints)
-        | Some c -> Now (Univ.UContext.constraints c)
+    let cstrs = Univ.UContext.constraints cb.const_universes in
+      Now cstrs ::  
+	(match cb.const_body with
+	| (Undef _ | Def _) -> []
+	| OpaqueDef lc ->
+	  match Opaqueproof.get_constraints lc with
+	  | None -> []
+	  | Some fc ->
+            match Future.peek_val fc with
+            | None -> [Later (Future.chain ~pure:true fc Univ.ContextSet.constraints)]
+            | Some c -> [Now (Univ.ContextSet.constraints c)])
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
-    Now Univ.Constraint.empty
+    [Now Univ.Constraint.empty]
   else
-    Now (Univ.UContext.constraints mb.mind_universes)
+    [Now (Univ.UContext.constraints mb.mind_universes)]
 
 let constraints_of_sfb sfb = 
   match sfb with
   | SFBconst cb -> globalize_constant_universes cb
   | SFBmind mib -> globalize_mind_universes mib
-  | SFBmodtype mtb -> Now mtb.typ_constraints
-  | SFBmodule mb -> Now mb.mod_constraints
+  | SFBmodtype mtb -> [Now mtb.typ_constraints]
+  | SFBmodule mb -> [Now mb.mod_constraints]
 
 (* let add_constraints cst senv = *)
 (*   { senv with *)
@@ -384,7 +390,7 @@ let add_field ((l,sfb) as field) gn senv =
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
   let cst = constraints_of_sfb sfb in
-  let senv = add_constraints cst senv in
+  let senv = add_constraints_list cst senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
     | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -757,7 +763,7 @@ let import lib cst vodigest senv =
   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 cst env in
+  let env = Environ.push_context_set cst env in
   (mp, lib.comp_natsymbs),
   { senv with
     env =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5b5457c38..429597f90 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -140,7 +140,7 @@ val export :
     module_path * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
-val import : compiled_library -> Univ.universe_context -> vodigest ->
+val import : compiled_library -> Univ.universe_context_set -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
 (** {6 Safe typing judgments } *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 780c14a20..0959fa703 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -57,6 +57,8 @@ let local_constrain_type env j = function
 
 (* Insertion of constants and parameters in environment. *)
 
+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 cbl = match se with
@@ -127,13 +129,14 @@ let infer_declaration env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
+        Future.chain ~greedy:true ~pure:true body (fun ((body, ctx), side_eff) ->
           let body = handle_side_effects env body side_eff in
-          let j = infer env body in
+	  let env' = push_context_set ctx env in
+          let j = infer env' body in
           let j = hcons_j j in
-          let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
+          let _typ = constrain_type env' j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, Univ.UContext.empty) in
+          j.uj_val, ctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
@@ -142,7 +145,8 @@ let infer_declaration env kn dcl =
       let env = push_context 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, side_eff = Future.join body in
+      let (body, ctx), side_eff = Future.join body in
+      let env = push_context_set ctx env in
       let body = handle_side_effects env body side_eff in
       let def, typ, proj = 
 	match c.const_entry_proj with
@@ -168,9 +172,12 @@ let infer_declaration env kn dcl =
 	  let def = Def (Mod_subst.from_val j.uj_val) in
 	    def, typ, None
       in
+      let univs = Univ.UContext.union c.const_entry_universes 
+	(Univ.ContextSet.to_context ctx)
+      in
 	feedback_completion_typecheck feedback_id;
 	def, typ, proj, c.const_entry_polymorphic,
-        c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
+        univs, c.const_entry_inline_code, c.const_entry_secctx
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
@@ -281,6 +288,6 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let handle_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
-    ce.const_entry_body (fun (body, side_eff) ->
-       handle_side_effects env body side_eff, Declareops.no_seff);
+    ce.const_entry_body (fun ((body, ctx), side_eff) ->
+      (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
 }
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index a2a35492e..8be1c76e0 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,6 +18,8 @@ val translate_local_def : env -> Id.t -> definition_entry ->
 
 val translate_local_assum : env -> types -> types
 
+val mk_pure_proof : constr -> proof_output
+
 (* returns the same definition_entry but with side effects turned into
  * let-ins or beta redexes. it is meant to get a term out of a not yet
  * type checked proof *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a7d96b55..c6355b3ea 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -427,11 +427,11 @@ let rec execute env cstr =
         let jl = execute_array env args in
 	let j =
 	  match kind_of_term f with
-	    | Ind ind when Environ.template_polymorphic_ind ind env ->
+	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 	      let args = Array.map (fun j -> lazy j.uj_type) jl in
 		judge_of_inductive_knowing_parameters env ind args
-	    | Const cst when Environ.template_polymorphic_constant cst env ->
+	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
 		(* Sort-polymorphism of constant *)
 	      let args = Array.map (fun j -> lazy j.uj_type) jl in
 		judge_of_constant_knowing_parameters env cst args
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 3d66b01cf..d931626e4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -680,7 +680,10 @@ struct
       external node : node -> data = "%identity"
       let hash = ExprHash.hash
       let uid = hash
-      let equal x y = x == y
+      let equal x y = x == y ||
+	(let (u,n) = x and (v,n') = y in
+	   Int.equal n n' && Level.equal u v)
+
       let stats _ = ()
       let init _ = ()
     end
@@ -716,9 +719,9 @@ struct
       | (l, 0) -> Level.is_small l
       | _ -> false
 
-    (* let equal (u,n) (v,n') = *)
-    (*   Int.equal n n' && Level.equal u v *)
-    let equal x y = x == y
+    let equal x y = x == y ||
+      (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
@@ -1244,18 +1247,6 @@ let check_eq_univs g l1 l2 =
     Huniv.for_all (fun x1 -> exists x1 l2) l1
     && Huniv.for_all (fun x2 -> exists x2 l1) l2
 
-  (* let exists x1 l = Huniv.exists_remove (fun x2 -> f x1 x2) l in *)
-  (*   try *)
-  (*     let l2' =  *)
-  (* 	Huniv.fold (fun x1 acc -> *)
-  (* 	  let l2' = exists x1 l2 in *)
-  (* 	    if l2 == l2' then raise Neq *)
-  (* 	    else l2') l1 l2 *)
-  (*     in  *)
-  (* 	if Huniv.is_nil l2' then true *)
-  (* 	else false (\* l2' has universes that are not equal to any in l1 *\) *)
-  (*   with Neq -> false *)
-
 (** [check_eq] is also used in [Evd.set_eq_sort],
     hence [Evarconv] and [Unification]. In this case,
     it seems that the Atom/Max case may occur,
@@ -1561,6 +1552,8 @@ module UniverseConstraints = struct
   include S
   
   let add (l,d,r as cst) s = 
+    if (Option.is_empty (Universe.level r)) then 
+      prerr_endline "Algebraic universe on the right";
     if Universe.equal l r then s
     else add cst s
 
@@ -2345,7 +2338,9 @@ let remove_large_constraint u v min =
 let is_direct_constraint u v =
   match Universe.level v with
   | Some u' -> Level.equal u u'
-  | None -> Huniv.mem (Universe.Expr.make u) v
+  | None -> 
+    let expr = Universe.Expr.make u in
+      Universe.exists (Universe.Expr.equal expr) v
 
 (*
    Solve a system of universe constraint of the form
@@ -2388,9 +2383,9 @@ let solve_constraints_system levels level_bounds level_min =
 let subst_large_constraint u u' v =
   match level u with
   | Some u ->
-      if is_direct_constraint u v then 
+      (* if is_direct_constraint u v then  *)
 	Universe.sup u' (remove_large_constraint u v type0m_univ)
-      else v
+      (* else v *)
   | _ ->
       anomaly (Pp.str "expect a universe level")
 
@@ -2477,7 +2472,7 @@ let hcons_universe_set =
 let hcons_universe_context_set (v, c) = 
   (hcons_universe_set v, hcons_constraints c)
 
-let hcons_univ x = x (* Universe.hcons (Huniv.node x) *)
+let hcons_univ x = Universe.hcons (Huniv.node x)
 
 let explain_universe_inconsistency (o,u,v,p) =
     let pr_rel = function
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ea3ab16a5..20ee554f1 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -433,6 +433,8 @@ val check_constraints : constraints -> universes -> bool
 val solve_constraints_system : universe option array -> universe array -> universe array ->
   universe array
 
+val remove_large_constraint : universe_level -> universe -> universe -> universe
+
 val subst_large_constraint : universe -> universe -> universe -> universe
 
 val subst_large_constraints :