- 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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cc46fe617f..9b5d7ffb08 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 *)
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index f534dd6c6f..1ddb59cf45 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 :=
+(* Polymorphic *) 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 :=
+(* Polymorphic *) 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 :=
+(* Polymorphic *) 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 :=
+(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
 (* Notations *)
@@ -65,7 +65,7 @@ Add Printing Let sigT2.
     [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
     proof of [(P a)] *)
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 Section Subset_projections.
 
   Variable A : Type.
@@ -215,7 +215,7 @@ Add Printing If sumor.
 Arguments inleft {A B} _ , [A] B _.
 Arguments inright {A B} _ , A [B] _.
 
-Unset Universe Polymorphism.
+(* Unset Universe Polymorphism. *)
 
 (** Various forms of the axiom of choice for specifications *)