Correct restriction of vm_compute when handling universe polymorphic

definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.

29 files changed, 94 insertions, 87 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 473a14c24..ae679027d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of inductive
+  | Const_ind of pinductive
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -67,7 +67,7 @@ type instruction =
                    (* nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of constant
+  | Kgetglobal of pconstant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (* size, tag *)
   | Kmakeprod
@@ -185,7 +185,7 @@ let rec instruction ppf = function
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
       print_string " bodies = ";
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
+  | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
   | Kconst cst ->
       fprintf ppf "\tconst"
   | Kmakeblock(n, m) ->
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 225198fcc..b65268f72 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of inductive
+  | Const_ind of pinductive
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -60,7 +60,7 @@ type instruction =
                    (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of constant
+  | Kgetglobal of pconstant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (** size, tag *)
   | Kmakeprod
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 39d800737..65ee655da 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -422,7 +422,7 @@ let rec str_const c =
               end
 	| _ -> Bconstr c
       end
-  | Ind (ind,u) -> Bstrconst (Const_ind ind)
+  | Ind ind -> Bstrconst (Const_ind ind)
   | Construct (((kn,j),i),u) ->  
       begin
       (* spiwack: tries first to apply the run-time compilation
@@ -486,12 +486,12 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env kn =
+let rec get_allias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     (match Cemitcodes.force tps with
     | BCallias kn' -> get_allias env kn'
-    | _ -> kn)
+    | _ -> p)
 
 (* Compiling expressions *)
 
@@ -700,10 +700,10 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_allias !global_env kn) :: cont
+      Kgetglobal (get_allias !global_env (kn, u)) :: cont
     else
       comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env kn) :: cont)
+                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
 let compile env c =
@@ -729,10 +729,10 @@ let compile_constant_body env = function
   | Def sb ->
       let body = Mod_subst.force_constr sb in
       match kind_of_term body with
-	| Const kn' ->
+	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
-	    let con= constant_of_kn (canonical_con (Univ.out_punivs kn')) in
-	      BCallias (get_allias env con)
+	    let con= constant_of_kn (canonical_con kn') in
+	      BCallias (get_allias env (con,u))
 	| _ ->
 	    let res = compile env body in
 	    let to_patch = to_memory res in
@@ -740,7 +740,7 @@ let compile_constant_body env = function
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias kn = BCallias (constant_of_kn (canonical_con kn))
+let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index d0bfd46c0..eab36d8b2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : constant -> body_code
+val compile_alias : pconstant -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
@@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env ->
            works as follow: checks if all the arguments are non-pointers
            if they are applies the operation (second argument) if not
            all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> constant -> bool -> comp_env ->
+val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
                              constr array -> int -> bytecodes-> bytecodes
 
 (*spiwack: compiling function to insert dynamic decompilation before
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 209144044..3c9692a5c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -20,7 +20,7 @@ open Mod_subst
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant
+  | Reloc_getglobal of pconstant
 
 type patch = reloc_info * int
 
@@ -147,8 +147,8 @@ and slot_for_annot a =
   enter (Reloc_annot a);
   out_int 0
 
-and slot_for_getglobal id =
-  enter (Reloc_getglobal id);
+and slot_for_getglobal p =
+  enter (Reloc_getglobal p);
   out_int 0
 
 
@@ -320,7 +320,7 @@ let rec subst_strcst s sc =
   match sc with
   | Const_sorts _ | Const_b0 _ -> sc
   | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
-  | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_mind s kn, i))
+  | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
 
 let subst_patch s (ri,pos) =
   match ri with
@@ -329,19 +329,19 @@ let subst_patch s (ri,pos) =
       let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
 
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant
+  | BCallias of pconstant
   | BCconstant
 
 let subst_body_code s = function
   | BCdefined tp -> BCdefined (subst_to_patch s tp)
-  | BCallias kn -> BCallias (fst (subst_con_kn s kn))
+  | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
   | BCconstant -> BCconstant
 
 type to_patch_substituted = body_code substituted
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 287c39304..cec901306 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant
+  | Reloc_getglobal of constant Univ.puniverses
 
 type patch = reloc_info * int
 
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant
+  | BCallias of constant Univ.puniverses
   | BCconstant
 
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 1c2eea17b..3b01538b9 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -40,12 +40,12 @@ let empty = {
   cst_trstate = Cpred.full;
 }
 
-let get_strategy { var_opacity; cst_opacity } = function
+let get_strategy { var_opacity; cst_opacity } f = function
   | VarKey id ->
       (try Id.Map.find id var_opacity
       with Not_found -> default)
   | ConstKey c ->
-      (try Cmap.find c cst_opacity
+      (try Cmap.find (f c) cst_opacity
       with Not_found -> default)
   | RelKey _ -> Expand
 
@@ -83,9 +83,11 @@ let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
 
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, expand the second one. *)
-let oracle_order o l2r k1 k2 =
-  match get_strategy o k1, get_strategy o k2 with
+let oracle_order f o l2r k1 k2 =
+  match get_strategy o f k1, get_strategy o f k2 with
     | Expand, _ -> true
     | Level n1, Opaque -> true
     | Level n1, Level n2 -> n1 < n2
     | _ -> l2r (* use recommended default *)
+
+let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 550076782..629912220 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -16,7 +16,8 @@ val empty : oracle
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : oracle -> bool -> constant tableKey -> constant tableKey -> bool
+val oracle_order : ('a -> constant) -> oracle -> bool -> 
+  'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
  * Higher levels means that the expansion is less prioritary.
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 794d94581..ed8b0a6d1 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,7 +57,7 @@ let set_global v =
 
 let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
@@ -67,7 +67,7 @@ let rec hash_structured_constant c =
   let open Hashset.Combine in
   match c with
   | Const_sorts s -> combinesmall 1 (Sorts.hash s)
-  | Const_ind i -> combinesmall 2 (ind_hash i)
+  | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
   | Const_b0 t -> combinesmall 3 (Int.hash t)
   | Const_bn (t, a) ->
     let fold h c = combine h (hash_structured_constant c) in
@@ -142,7 +142,7 @@ let slot_for_annot key =
     AnnotTable.add annot_tbl key n;
     n
 
-let rec slot_for_getglobal env kn =
+let rec slot_for_getglobal env (kn,u) =
   let (cb,(_,rk)) = lookup_constant_key kn env in
   try key rk
   with NotEvaluated ->
@@ -150,10 +150,12 @@ let rec slot_for_getglobal env kn =
     let pos =
       match Cemitcodes.force cb.const_body_code with
       | BCdefined(code,pl,fv) ->
-	let v = eval_to_patch env (code,pl,fv) in
-	set_global v
+	if Univ.Instance.is_empty u then
+	  let v = eval_to_patch env (code,pl,fv) in
+	    set_global v
+	else set_global (val_of_constant (kn,u))
     | BCallias kn' -> slot_for_getglobal env kn'
-    | BCconstant -> set_global (val_of_constant kn) in
+    | BCconstant -> set_global (val_of_constant (kn,u)) in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
     pos
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 8b1e49919..0ebff440a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -594,7 +594,7 @@ let dispatch =
   let int31_op n op prim kn =
     { empty_reactive_info with
       vm_compiling = Some (Cbytegen.op_compilation n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim kn);
+      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
     }
   in
 
@@ -602,7 +602,7 @@ fun rk value field ->
   (* subfunction which shortens the (very common) dispatch of operations *)
   let int31_op_from_const n op prim =
     match kind_of_term value with
-      | Const (kn,_) ->  int31_op n op prim kn
+      | Const kn ->  int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e04eb354e..392e667b8 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver =
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
+	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/names.ml b/kernel/names.ml
index 2c2886623..b349ccb00 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -686,8 +686,6 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 			  starting by the end, {\em inverse}
 			  of de Bruijn indice *)
 
-type id_key = Constant.t tableKey
-
 let eq_table_key f ik1 ik2 =
   if ik1 == ik2 then true
   else match ik1,ik2 with
@@ -696,8 +694,6 @@ let eq_table_key f ik1 ik2 =
   | RelKey k1, RelKey k2 -> Int.equal k1 k2
   | _ -> false
 
-let eq_id_key = eq_table_key Constant.UserOrd.equal
-
 let eq_con_chk = Constant.UserOrd.equal
 let eq_mind_chk = MutInd.UserOrd.equal
 let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index 9fbe7d5e5..d82043da1 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment
 			  starting by the end, {e inverse}
 			  of de Bruijn indice *)
 
-type id_key = Constant.t tableKey
-
 val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
 val eq_constant_key : Constant.t -> Constant.t -> bool
-val eq_id_key : id_key -> id_key -> bool
 
 (** equalities on constant and inductive names (for the checker) *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 433e2c505..66577fecc 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
   | None ->
     begin match cb.const_body with
-    | Def t ->
+    | Def t when not cb.const_polymorphic ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
       if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
@@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive
 let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
-  | Const (c,u) ->
-      let c = get_allias env c in
+  | Const c ->
+      let c,u = get_allias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index c5417b2b6..947e0a148 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,11 +373,11 @@ let makeblock env cn tag args =
 
 (* Translation of constants *)
 
-let rec get_allias env kn =
+let rec get_allias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
   match Cemitcodes.force tps with
   |  Cemitcodes.BCallias kn' -> get_allias env kn'
-  | _ -> kn
+  | _ -> p
 
 (*i Global environment *)
 
@@ -647,8 +647,8 @@ let rec lambda_of_constr env sigma c =
 
 and lambda_of_app env sigma f args =
   match kind_of_term f with
-  | Const (kn,u) ->
-      let kn = get_allias !global_env kn in
+  | Const (kn,u as c) ->
+      let kn,u = get_allias !global_env c in
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 10818e1aa..6a97edc40 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -27,7 +27,7 @@ val mk_lazy : lambda -> lambda
 
 val get_mind_prefix : env -> mutual_inductive -> string
 
-val get_allias : env -> constant -> constant
+val get_allias : env -> pconstant -> pconstant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 62f454047..4153b323b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -350,7 +350,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = Closure.oracle_of_infos infos in
          let (app1,app2) =
-           if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then
+           if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
              | Some def1 -> ((lft1, whd def1 v1), appr2)
              | None ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d5939c67e..e2a19b0e8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1744,6 +1744,8 @@ type universe_instance = Instance.t
 type 'a puniverses = 'a * Instance.t
 let out_punivs (x, y) = x
 let in_punivs x = (x, Instance.empty)
+let eq_puniverses f (x, u) (y, u') =
+  f x y && Instance.equal u u'
 
 (** A context of universe levels with universe constraints,
     representiong local universe variables and constraints *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 36f3349c0..454134f21 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -306,6 +306,8 @@ type 'a puniverses = 'a * universe_instance
 val out_punivs : 'a puniverses -> 'a
 val in_punivs : 'a -> 'a puniverses
 
+val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
+
 (** A vector of universe levels with universe constraints,
     representiong local universe variables and associated constraints *)
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 1685817a3..88c1e1038 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -336,3 +336,6 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
+
+type id_key = pconstant tableKey
+let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index bdbecdedc..fdd4603b5 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -87,3 +87,6 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : universe_instance -> constr -> constr
 val subst_instance_context : universe_instance -> rel_context -> rel_context
+
+type id_key = pconstant tableKey
+val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 3f9345ff8..80b15f8ba 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -86,23 +86,24 @@ and conv_whd env pb k whd1 whd2 cu =
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
-  | Aind (kn1,i1), Aind(kn2,i2) ->
-      if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+  | Aind ind1, Aind ind2 ->
+      if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
       then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 ->
-      if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+      if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
       begin
 	try
-	  if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then
+	  if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	    conv_stack env k stk1 stk2 cu
 	  else raise NotConvertible
 	with NotConvertible ->
-	  if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
+	  if oracle_order Univ.out_punivs (oracle_of_infos !infos) 
+	    false ik1 ik2 then
             conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
           else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
diff --git a/kernel/vm.ml b/kernel/vm.ml
index a7e5a55c4..2cc1efe43 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -137,10 +137,11 @@ type vswitch = {
 (* Generally the first field is a code pointer.                           *)
 
 (* Do not edit this type without editing C code, especially "coq_values.h" *)
+
 type atom =
-  | Aid of id_key
-  | Aiddef of id_key * values
-  | Aind of inductive
+  | Aid of Vars.id_key
+  | Aiddef of Vars.id_key * values
+  | Aind of pinductive
 
 (* Zippers *)
 
@@ -306,11 +307,11 @@ let val_of_atom a = val_of_obj (obj_of_atom a)
 
 module IdKeyHash =
 struct
-  type t = id_key
-  let equal = Names.eq_id_key
+  type t = pconstant tableKey
+  let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
   open Hashset.Combine
   let hash = function
-  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
 end
diff --git a/kernel/vm.mli b/kernel/vm.mli
index fa88418ce..295ea83c4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -24,9 +24,9 @@ type vswitch
 type arguments
 
 type atom =
-  | Aid of id_key
-  | Aiddef of id_key * values
-  | Aind of inductive
+  | Aid of Vars.id_key
+  | Aiddef of Vars.id_key * values
+  | Aind of pinductive
 
 (** Zippers *)
 
@@ -54,7 +54,7 @@ type whd =
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
-val val_of_constant : constant -> values
+val val_of_constant : pconstant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3f9f7ff28..203b1ec8a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -511,8 +511,8 @@ let oracle_order env cf1 cf2 =
 	  when eq_constant p (Projection.constant p') -> 
 	  Some (Projection.unfolded p')
 	| _ ->
-          Some (Conv_oracle.oracle_order (Environ.oracle env) false
-		  (translate_key k1) (translate_key k2))
+          Some (Conv_oracle.oracle_order (fun x -> x)
+		  (Environ.oracle env) false (translate_key k1) (translate_key k2))
 
 let is_rigid_head flags t =
   match kind_of_term t with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1d97aef27..3f1e6e5d6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,12 +93,11 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-(* FIXME: treatment of universes *)
 let constr_type_of_idkey env idkey =
   match idkey with
   | ConstKey cst ->
-    let const_type = (Environ.lookup_constant cst env).const_type in
-      mkConst cst, Typeops.type_of_constant_type env const_type
+    let const_type = Typeops.type_of_constant_in env cst in
+      mkConstU cst, const_type
   | VarKey id ->
       let (_,_,ty) = lookup_named id env in
       mkVar id, ty
@@ -107,7 +106,7 @@ let constr_type_of_idkey env idkey =
       let (_,_,ty) = lookup_rel n env in
       mkRel n, lift n ty
 
-let type_of_ind env ind u =
+let type_of_ind env (ind, u) =
   type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
 
 let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
@@ -176,7 +175,7 @@ and nf_whd env whd typ =
   | Vatom_stk(Aiddef(idkey,v), stk) ->
       nf_whd env (whd_stack v stk) typ
   | Vatom_stk(Aind ind, stk) ->
-      nf_stk env (mkInd ind) (type_of_ind env ind Univ.Instance.empty (*FIXME*)) stk
+      nf_stk env (mkIndU ind) (type_of_ind env ind) stk
 
 and nf_stk env c t stk  =
   match stk with
@@ -194,7 +193,7 @@ and nf_stk env c t stk  =
       let nparams = mib.mind_nparams in
       let params,realargs = Util.Array.chop nparams allargs in
       let pT =
-	hnf_prod_applist env (type_of_ind env ind u) (Array.to_list params) in
+	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
       let pT = whd_betadeltaiota env pT in
       let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index a04535f40..de615301d 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -342,8 +342,8 @@ Arguments identity_rect [A] a P f y i.
 
 (** Identity type *)
 
-Polymorphic Definition ID := forall A:Type, A -> A.
-Polymorphic Definition id : ID := fun A x => x.
+Definition ID := forall A:Type, A -> A.
+Definition id : ID := fun A x => x.
 
 Definition IDProp := forall A:Prop, A -> A.
 Definition idProp : IDProp := fun A x => x.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 47e302e32..1384901b7 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -21,19 +21,19 @@ Require Import Logic.
     Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
     of elements of the type [A] which satisfy both [P] and [Q]. *)
 
-(* Polymorphic *) Inductive sig (A:Type) (P:A -> Prop) : Type :=
+Inductive sig (A:Type) (P:A -> Prop) : Type :=
     exist : forall x:A, P x -> sig P.
 
-(* Polymorphic *) Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
+Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
 (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
     Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
-(* Polymorphic *) Inductive sigT (A:Type) (P:A -> Type) : Type :=
+Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT P.
 
-(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
+Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
 (* Notations *)
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 4bc29a071..e5be0ca92 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -15,8 +15,6 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* Set Universe Polymorphism. *)
-
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
 Arguments id {A} x.
@@ -47,7 +45,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
 
 (** The [flip] combinator reverses the first two arguments of a function. *)
 
-Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x.
+Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
 (** Application as a combinator. *)