3 files changed, 22 insertions, 14 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index ab424c223..7e4475d40 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1284,7 +1284,7 @@ Qed.
 
 (* Extraire une hypothèse de la liste *)
 Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.
-
+Unset Printing Notations.
 Theorem nth_valid :
  forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
  interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5416e936c..689462704 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -30,11 +30,11 @@ let string_of_global r =
 let destructurate t =
   let c, args = Term.decompose_app t in
   match Term.kind_of_term c, args with
-    | Term.Const sp, args ->
+    | Term.Const (sp,_), args ->
 	Kapp (string_of_global (Globnames.ConstRef sp), args)
-    | Term.Construct csp , args ->
+    | Term.Construct (csp,_) , args ->
 	Kapp (string_of_global (Globnames.ConstructRef csp), args)
-    | Term.Ind isp, args ->
+    | Term.Ind (isp,_), args ->
 	Kapp (string_of_global (Globnames.IndRef isp), args)
     | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -48,9 +48,9 @@ let dest_const_apply t =
   let f,args = Term.decompose_app t in
   let ref =
   match Term.kind_of_term f with
-    | Term.Const sp      -> Globnames.ConstRef sp
-    | Term.Construct csp -> Globnames.ConstructRef csp
-    | Term.Ind isp       -> Globnames.IndRef isp
+    | Term.Const (sp,_)      -> Globnames.ConstRef sp
+    | Term.Construct (csp,_) -> Globnames.ConstructRef csp
+    | Term.Ind (isp,_)       -> Globnames.IndRef isp
     | _ -> raise Destruct
   in  Nametab.basename_of_global ref, args
 
@@ -210,19 +210,26 @@ let rec mk_nat = function
 
 (* Lists *)
 
-let coq_cons =  lazy (constant "cons")
-let coq_nil =  lazy (constant "nil")
+let mkListConst c u = 
+  Term.mkConstructU (Globnames.destConstructRef 
+		     (Coqlib.gen_reference "" ["Init";"Datatypes"] c),
+		     Univ.Instance.of_array [|u|])
 
-let mk_list typ l =
+let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
+let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])
+
+let mk_list univ typ l =
   let rec loop = function
-    | [] ->
-	Term.mkApp (Lazy.force coq_nil, [|typ|])
+    | [] -> coq_nil univ typ
     | (step :: l) ->
-	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
+	Term.mkApp (coq_cons univ typ, [| step; loop l |]) in
   loop l
 
-let mk_plist l = mk_list Term.mkProp l
+let mk_plist = 
+  let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
+    fun l -> mk_list type1lev Term.mkProp l
 
+let mk_list = mk_list Univ.Level.set
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index b8db71e40..4ae1cb94c 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -117,6 +117,7 @@ val do_seq : Term.constr -> Term.constr -> Term.constr
 val do_list : Term.constr list -> Term.constr
 
 val mk_nat : int -> Term.constr
+(** Precondition: the type of the list is in Set *)
 val mk_list : Term.constr -> Term.constr list -> Term.constr
 val mk_plist : Term.types list -> Term.types
 val mk_shuffle_list : Term.constr list -> Term.constr