Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel

19 files changed, 155 insertions, 238 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b9e7ec1691..95822fac68 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -184,13 +184,14 @@ let lift_univs cb subst =
     if (Univ.LMap.is_empty subst) then
       subst, (Polymorphic_const auctx)
     else
-      let inst = Univ.AUContext.instance auctx in
       let len = Univ.LMap.cardinal subst in
-      let subst = 
-        Array.fold_left_i 
-          (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
-	  subst (Univ.Instance.to_array inst)
+      let rec gen_subst i acc =
+        if i < 0 then acc
+        else
+          let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
+          gen_subst (pred i) acc
       in
+      let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
       let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
       subst, (Polymorphic_const auctx')
 
@@ -249,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } =
   let univs =
     match univs with
     | Monomorphic_const ctx -> 
-      Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx)
+      assert (AUContext.is_empty abs_ctx); univs
     | Polymorphic_const auctx -> 
       Polymorphic_const (AUContext.union abs_ctx auctx)
   in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1337036b8b..efce219826 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -44,47 +44,19 @@ let hcons_template_arity ar =
 
 (** {6 Constants } *)
 
-let instantiate cb c =
-  match cb.const_universes with
-  | Monomorphic_const _ -> c
-  | Polymorphic_const ctx -> 
-     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
-
 let constant_is_polymorphic cb =
   match cb.const_universes with
   | Monomorphic_const _ -> false
   | Polymorphic_const _ -> true
 
-let body_of_constant otab cb = match cb.const_body with
-  | Undef _ -> None
-  | Def c -> Some (instantiate cb (force_constr c))
-  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
-
-let type_of_constant cb =
-  match cb.const_type with
-  | RegularArity t as x -> 
-    let t' = instantiate cb t in
-      if t' == t then x else RegularArity t'
-  | TemplateArity _ as x -> x
-
-let universes_of_polymorphic_constant otab cb = 
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
-
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
   | Def _ | OpaqueDef _ -> true
 
-let constant_polymorphic_instance cb =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_polymorphic_context cb =
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
@@ -268,19 +240,11 @@ let subst_mind_body sub mib =
     mind_typing_flags = mib.mind_typing_flags;
   }
 
-let inductive_polymorphic_instance mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
-  | Cumulative_ind cumi -> 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
 let inductive_polymorphic_context mib =
   match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  | Monomorphic_ind _ -> Univ.AUContext.empty
+  | Polymorphic_ind ctx -> ctx
+  | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi
 
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 7350724b8b..a8ba5fa392 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,25 +27,14 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
-val constant_polymorphic_instance : constant_body -> universe_instance
-val constant_polymorphic_context : constant_body -> universe_context
+val constant_polymorphic_context : constant_body -> abstract_universe_context
 
 (** Is the constant polymorphic? *)
 val constant_is_polymorphic : constant_body -> bool
 
-(** Accessing const_body, forcing access to opaque proof term if needed.
-    Only use this function if you know what you're doing. *)
-
-val body_of_constant :
-  Opaqueproof.opaquetab -> constant_body -> Term.constr option
-val type_of_constant : constant_body -> constant_type
-
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val universes_of_polymorphic_constant :
-  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
-
 val is_opaque : constant_body -> bool
 
 (** Side effects *)
@@ -68,8 +57,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
-val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context
 
 (** Is the inductive polymorphic? *)
 val inductive_is_polymorphic : mutual_inductive_body -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd204c7d59..b01b652001 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -230,8 +230,7 @@ let add_constant kn cb env =
 let constraints_of cb u =
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -248,17 +247,11 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
-let constant_instance env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_context env kn =
   let cb = lookup_constant kn env in
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 type const_evaluation_result = NoBody | Opaque | IsProj
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f8887d8e83..cd7a9d2791 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -160,10 +160,7 @@ val constant_value_and_type : env -> constant puniverses ->
   constr option * constant_type * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> constant -> Univ.universe_context
-(** The universe isntance associated to the constant, empty if not 
-    polymorphic *)
-val constant_instance : env -> constant -> Univ.universe_instance
+val constant_context : env -> constant -> Univ.abstract_universe_context
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 04971f83dc..e248436ec4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -961,13 +961,10 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u =
-        let process auctx = 
-          subst_univs_level_instance substunivs (Univ.AUContext.instance auctx)
-        in
         match aiu with
         | Monomorphic_ind _ -> Univ.Instance.empty
-        | Polymorphic_ind auctx -> process auctx
-        | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi)
+        | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+        | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
       in
       let indsp = ((kn, 0), u) in
       let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be1..1eaba49aa9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx = 
-    Univ.UContext.constraints (Univ.subst_instance_context u auctx)
-  in
+  let process auctx =  Univ.AUContext.instantiate u auctx in
   match mib.mind_universes with
   | Monomorphic_ind _ -> Univ.Constraint.empty
   | Polymorphic_ind auctx -> process auctx
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 71c0370083..c7f3e5c51b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,37 +92,29 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	         c, Reduction.infer_conv env' (Environ.universes env') c c'
 	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
         | Polymorphic_const uctx ->
-          let uctx = Univ.instantiate_univ_context uctx in
-	  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 (UGraph.check_constraints cst (Environ.universes env')) then
-		     error_incorrect_with_constraint lab
-	  in
+          let subst, ctx = Univ.abstract_universes ctx in
+          let c = Vars.subst_univs_level_constr subst c in
+          let () =
+            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+              error_incorrect_with_constraint lab
+          in
+          (** Terms are compared in a context with De Bruijn universe indices *)
+	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env 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 typ = Vars.subst_instance_constr cus typ 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 c' = Mod_subst.force_constr cs in
 	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
 	        cst'
 	  in
 	    if not (Univ.Constraint.is_empty cst) then
 	      error_incorrect_with_constraint lab;
-	    let subst, ctx = Univ.abstract_universes ctx in
-	      Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
+            c, Polymorphic_const ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
 (*      let ctx' = Univ.UContext.make (newus, cst) in *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 24be46933e..a079bc8931 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -49,7 +49,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 4a150d54bd..e2a94b6919 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -108,7 +108,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1acede729a..da7fcd6f23 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1861,10 +1861,10 @@ and compile_named env sigma univ auxdefs id =
 let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
   | None ->
-     let u =
+     let no_univs =
        match cb.const_universes with
-       | Monomorphic_const _ -> Univ.Instance.empty
-       | Polymorphic_const ctx -> Univ.AUContext.instance ctx
+       | Monomorphic_const _ -> true
+       | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0
      in
     begin match cb.const_body with
     | Def t ->
@@ -1879,7 +1879,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       in
       let l = con_label con in
       let auxdefs,code =
-	if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code
+	if no_univs then compile_with_fv env sigma None [] (Some l) code
 	else
 	  let univ = fresh_univ () in
 	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
@@ -1894,7 +1894,7 @@ let compile_constant env sigma prefix ~interactive con cb =
     | _ -> 
         let i = push_symbol (SymbConst con) in
 	let args =
-	  if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|]
+	  if no_univs then [|get_const_code i; MLarray [||]|]
 	  else [|get_const_code i|]
 	in
 	(*
@@ -1959,14 +1959,14 @@ let param_name = Name (id_of_string "params")
 let arg_name = Name (id_of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
-  let u = Declareops.inductive_polymorphic_instance mb in
+  let u = Declareops.inductive_polymorphic_context mb in
   let f i stack ob =
     let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd (mind,i)) in
     let name = Gind ("", (mind, i)) in
     let accu =
       let args =
-	if Univ.Instance.is_empty u then
+	if Int.equal (Univ.AUContext.size u) 0 then
 	  [|get_ind_code j; MLarray [||]|]
 	else [|get_ind_code j|]
       in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index de4efbba93..2bf9f43a5a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -680,8 +680,7 @@ let infer_check_conv_constructors
 
 let check_inductive_instances cv_pb cumi u u' univs =
   let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
@@ -690,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints 
-            (Univ.subst_instance_context comp_subst ind_subtypctx) 
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
         in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
@@ -767,8 +764,7 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
 
 let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
   let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
@@ -777,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints
-            (Univ.subst_instance_context comp_subst ind_subtypctx) in
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6f128d5d30..bd82dd465b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -80,10 +80,8 @@ let make_labmap mp list =
   List.fold_right add_one list empty_labmap
 
 
-let check_conv_error error why cst poly u f env a1 a2 =
+let check_conv_error error why cst poly f env a1 a2 =
   try 
-    let a1 = Vars.subst_instance_constr u a1 in
-    let a2 = Vars.subst_instance_constr u a2 in
     let cst' = f env (Environ.universes env) a1 a2 in
       if poly then 
 	if Constraint.is_empty cst' then cst
@@ -92,36 +90,42 @@ let check_conv_error error why cst poly u f env a1 a2 =
   with NotConvertible -> error why
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error IncompatibleInstances
+  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints auctx1)
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = KerName.make2 mp1 l in
   let kn2 = KerName.make2 mp2 l in
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv why cst poly u f = check_conv_error error why cst poly u f in
+  let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
-  let u =
-    let process inst inst' =
-      if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances
-    in
+  let env, inst =
     match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
     | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      process
-        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      process
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | _ -> error 
              (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
-  let check_inductive_type cst name env t1 t2 =
+  let check_inductive_type cst name t1 t2 =
 
     (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
@@ -154,7 +158,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -172,21 +176,20 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let ty1, cst1 = constrained_type_of_inductive env ((mib1,p1),u) in
-      let ty2, cst2 = constrained_type_of_inductive env ((mib2,p2),u) in
-      let cst = Constraint.union cst1 (Constraint.union cst2 cst) in
-      let cst = check_inductive_type cst p2.mind_typename env ty1 ty2 in
+      let ty1 = type_of_inductive env ((mib1, p1), inst) in
+      let ty2 = type_of_inductive env ((mib2, p2), inst) in
+      let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
 	cst
   in
   let mind = mind_of_kn kn1 in
   let check_cons_types i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	(inductive_is_polymorphic mib1) u infer_conv env t1 t2)
+	(inductive_is_polymorphic mib1) infer_conv env t1 t2)
       cst
       p2.mind_consnames
-      (arities_of_specif (mind,u) (mib1,p1))
-      (arities_of_specif (mind,u) (mib2,p2))
+      (arities_of_specif (mind, inst) (mib1, p1))
+      (arities_of_specif (mind, inst) (mib2, p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
   check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
@@ -242,8 +245,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv cst poly u f = check_conv_error error cst poly u f in
-  let check_type poly u cst env t1 t2 =
+  let check_conv cst poly f = check_conv_error error cst poly f in
+  let check_type poly cst env t1 t2 =
 
     let err = NotConvertibleTypeField (env, t1, t2) in
 
@@ -290,7 +293,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	  t1,t2
       else
         (t1,t2) in
-      check_conv err cst poly u infer_conv_leq env t1 t2
+      check_conv err cst poly infer_conv_leq env t1 t2
   in
   match info1 with
     | Constant cb1 ->
@@ -298,48 +301,21 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking universes *)
-      let poly = 
-	if not (Declareops.constant_is_polymorphic cb1 
-                 == Declareops.constant_is_polymorphic cb2) then
-           error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2))
-	else Declareops.constant_is_polymorphic cb2
-      in
-      let cst', env', u =
+      let poly, env =
         match cb1.const_universes, cb2.const_universes with
         | Monomorphic_const _, Monomorphic_const _ ->
-          cst, env, Univ.Instance.empty
+          false, env
         | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
-          begin
-	    let ctx1 = Univ.instantiate_univ_context auctx1 in
-	    let ctx2 = Univ.instantiate_univ_context auctx2 in
-	    let inst1, ctx1 = Univ.UContext.dest ctx1 in
-	    let inst2, ctx2 = Univ.UContext.dest ctx2 in
-	    if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
-	      error IncompatibleInstances
-	    else 
-	      let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
-	      let cstrs = Univ.Constraint.union cstrs ctx2 in
-	      try 
-		(* The environment with the expected universes plus equality 
-		   of the body instances with the expected instance *)
-		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 UGraph.check_constraints ctx1 (Environ.universes env) then
-		  cstrs, env, inst2
-		else error (IncompatibleConstraints ctx1)
-	      with Univ.UniverseInconsistency incon -> 
-		error (IncompatibleUniverses incon)
-          end
-        | _ -> assert false
+          true, check_polymorphic_instance error env auctx1 auctx2
+        | Monomorphic_const _, Polymorphic_const _ ->
+          error (PolymorphicStatusExpected true)
+        | Polymorphic_const _, Monomorphic_const _ ->
+          error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env' cb2.const_type in
-      let cst = check_type poly u cst env' typ1 typ2 in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
 	   transparent constant.
@@ -356,7 +332,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		 Anyway [check_conv] will handle that afterwards. *)
 	      let c1 = Mod_subst.force_constr lc1 in
 	      let c2 = Mod_subst.force_constr lc2 in
-	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
+	      check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 6590d7e712..b24c20aa02 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -11,5 +11,3 @@ open Declarations
 open Environ
 
 val check_subtypes : env -> module_type_body -> module_type_body -> constraints
-
-
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 283febed24..3e516cae04 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -131,8 +131,7 @@ let inline_side_effects env body ctx side_eff =
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
       | Polymorphic_const auctx ->
         (** Inline the term to emulate universe polymorphism *)
-        let data = (Univ.AUContext.instance auctx, b) in
-        let subst = Cmap_env.add c (Inl data) subst in
+        let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
     in
     let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
@@ -142,7 +141,7 @@ let inline_side_effects env body ctx side_eff =
       let data = try Some (Cmap_env.find c subst) with Not_found -> None in
       begin match data with
       | None -> t
-      | Some (Inl (inst, b)) ->
+      | Some (Inl b) ->
         (** [b] is closed but may refer to other constants *)
         subst_const i k (Vars.subst_instance_constr u b)
       | Some (Inr n) ->
@@ -470,7 +469,7 @@ let constant_entry_of_side_effect cb u =
     match cb.const_universes with
     | Monomorphic_const ctx -> false, ctx
     | Polymorphic_const auctx -> 
-      true, Univ.instantiate_univ_context auctx
+      true, Univ.AUContext.repr auctx
   in
   let pt =
     match cb.const_body, u with
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 487257a776..9793dd881d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -830,6 +830,18 @@ let sort_universes g =
   in
   normalize_universes g
 
+(** Subtyping of polymorphic contexts *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = UContext.dest (AUContext.repr ctx) in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs (Instance.to_array inst) in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Instances *)
 
 let check_eq_instances g t1 t2 =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 935a3cab4a..4de373eb4c 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool
 val check_eq_instances : Instance.t check_function
 (** Check equality of instances w.r.t. a universe graph *)
 
+val check_subtype : AUContext.t check_function
+(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
+    [ctx1]. *)
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1c887e2a99..6614d60276 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -988,6 +988,31 @@ let enforce_eq_instances x y =
 		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1031,7 +1056,18 @@ end
 type universe_context = UContext.t
 let hcons_universe_context = UContext.hcons
 
-module AUContext = UContext
+module AUContext =
+struct
+  include UContext
+
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
 
 type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
@@ -1256,31 +1292,6 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
-
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1378,19 +1389,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 let compare_levels = Level.compare
 let eq_levels = Level.equal
 let equal_universes = Universe.equal
-
-
-let subst_instance_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_constraints
-  else subst_instance_constraints
-
-let subst_instance_context = 
-  let subst_instance_context_body inst (inner_inst, inner_constr) =
-    (inner_inst, subst_instance_constraints inst inner_constr)
-  in
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_context_body
-  else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index d7ee3eceec..53297ac462 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -319,15 +319,24 @@ module AUContext :
 sig 
   type t
 
+  val repr : t -> UContext.t
+  (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of
+      the context and [cstr] the abstracted constraints. *)
+
   val empty : t
+  val is_empty : t -> bool
 
+  (** Don't use. *)
   val instance : t -> Instance.t
-                        
+
   val size : t -> int
 
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
+  val instantiate : Instance.t -> t -> Constraint.t
+  (** Generate the set of instantiated constraints **)
+
 end
 
 type abstract_universe_context = AUContext.t
@@ -442,7 +451,6 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 val make_instance_subst : universe_instance -> universe_level_subst
 val make_inverse_instance_subst : universe_instance -> universe_level_subst
@@ -453,10 +461,10 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs
 
 val make_abstract_instance : abstract_universe_context -> universe_instance
 
-(** Get the instantiated graph. *)
+(** Don't use. *)
 val instantiate_univ_context : abstract_universe_context -> universe_context
 
-(** Get the instantiated graphs for both universe constraints and subtyping constraints. *)
+(** Don't use. *)
 val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
 
 (** {6 Pretty-printing of universes. } *)