- 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, 2 insertions, 2 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cc46fe617..9b5d7ffb0 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -143,7 +143,7 @@ Arguments S _%nat.
 (********************************************************************)
 (** * Container datatypes *)
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 (** [option A] is the extension of [A] with an extra element [None] *)
 
@@ -250,7 +250,7 @@ Definition app (A : Type) : list A -> list A -> list A :=
 
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
-Unset Universe Polymorphism.
+(* Unset Universe Polymorphism. *)
 
 (********************************************************************)
 (** * The comparison datatype *)