- 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

1 files changed, 9 insertions, 4 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 689462704..3fa9e02cf 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -210,10 +210,15 @@ let rec mk_nat = function
 
 (* Lists *)
 
-let mkListConst c u = 
-  Term.mkConstructU (Globnames.destConstructRef 
-		     (Coqlib.gen_reference "" ["Init";"Datatypes"] c),
-		     Univ.Instance.of_array [|u|])
+let mkListConst c = 
+  let r = 
+    Coqlib.gen_reference "" ["Init";"Datatypes"] c
+  in 
+  let inst = 
+    if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
+    else fun _ -> Univ.Instance.empty
+  in
+    fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u)
 
 let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
 let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])