- 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

14 files changed, 21 insertions, 21 deletions

diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 73be830a4..cbde5f9ab 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -62,7 +62,7 @@ Instance snd_measure : @Measure (A * B) B Snd.
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
 
-Polymorphic Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
+Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
  relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
 
 Infix "*" := RelProd : signature_scope.
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 *)
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index f534dd6c6..1ddb59cf4 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 *)
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f6a0382c2..2062f3861 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -10,7 +10,7 @@ Require Import Le Gt Minus Bool.
 Require Setoid.
 
 Set Implicit Arguments.
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 (******************************************************************)
 (** * Basics: definition of polymorphic lists and some operations *)
@@ -2036,4 +2036,4 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
 Hint Resolve app_nil_end : datatypes v62.
 (* end hide *)
 
-Unset Universe Polymorphism.
+(* Unset Universe Polymorphism. *)
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index ba62fa7fd..644d479c6 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -11,7 +11,7 @@ Require Export Sorted.
 Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 (** * Logical relations over lists with respect to a setoid equality
       or ordering. *)
 
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index 05f03ea56..afc7c25bd 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 
 Require Import SetoidList.
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 57a82161d..d8416b3e2 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -100,7 +100,7 @@ Local Unset Intuition Negation Unfolding.
     so they require polymorphism otherwise their first application (e.g. to an
     existential in [Set]) will fix the level of [A].
 *)
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 Section ChoiceSchemes.
 
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index bd6e2ca8f..2f61e0e29 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -52,7 +52,7 @@ Table of contents:
 
 Import EqNotations.
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 Section Dependent_Equality.
 
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index e4db81faf..0758bd1f9 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -35,7 +35,7 @@ Table of contents:
 (** * Streicher's K and injectivity of dependent pair hold on decidable types *)
 
 Set Implicit Arguments.
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 Section EqdepDec.
 
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index d8f675ade..ed09030cb 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1047,7 +1047,7 @@ Qed.
 
 (** ** Filter *)
 
-Polymorphic Lemma filter_app A f (l l':list A) :
+Lemma filter_app A f (l l':list A) :
  List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
 Proof.
  induction l as [|x l IH]; simpl; trivial.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index ab1eccee2..a86ae783e 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -15,7 +15,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 899acfc64..a7eddd9f0 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -16,7 +16,7 @@
 Require Import List Setoid Compare_dec Morphisms FinFun.
 Import ListNotations. (* For notations [] and [a;b;c] *)
 Set Implicit Arguments.
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 Section Permutation.
 
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 5b52c6ec9..beed92b84 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -20,7 +20,7 @@
 
 Require Import List Relations Relations_1.
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 (** Preambule *)
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index f12aa0b87..6d2146b8e 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -21,7 +21,7 @@ Require Vectors.Fin.
 Import EqNotations.
 Local Open Scope nat_scope.
 
-Set Universe Polymorphism.
+(* Set Universe Polymorphism. *)
 
 (**
 A vector is a list of size n whose elements belong to a set A. *)