fixing universe polymorphism for 8.5pl1

Author: gmalecha

theories/Core/Type.v

@@ -24,7 +24,7 @@ Existing Class proper.
 
 Section type.
   Polymorphic Context {T : Type}.
-  Variable tT : type T.
+  Polymorphic Variable tT : type T.
 (*
   Global Instance Proper_type : Proper T :=
   { proper := fun x => equal x x }.

theories/Data/HList.v

@@ -12,6 +12,7 @@ Require Import ExtLib.Tactics.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Universe Polymorphism.
 
 (** Core Type and Functions **)
 Section hlist.

theories/Data/List.v

@@ -134,10 +134,10 @@ Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.Applicative.
 
 Section traversable.
-  Context {F : Type -> Type}.
-  Context {Applicative_F : Applicative F}.
-  Context {A B : Type}.
-  Variable f : A -> F B.
+  Polymorphic Context {F : Type -> Type}.
+  Polymorphic Context {Applicative_F : Applicative F}.
+  Polymorphic Context {A B : Type}.
+  Polymorphic Variable f : A -> F B.
 
   Polymorphic Fixpoint mapT_list (ls : list A) : F (list B) :=
     match ls with

theories/Data/POption.v

@@ -5,7 +5,7 @@ Set Printing Universes.
 
 Section poption.
   Polymorphic Universe i.
-  Variable T : Type@{i}.
+  Polymorphic Variable T : Type@{i}.
 
   Polymorphic Inductive poption : Type@{i} :=
   | pSome : T -> poption
@@ -18,8 +18,8 @@ Arguments pNone {_}.
 
 Section poption_map.
   Polymorphic Universes i j.
-  Context {T : Type@{i}} {U : Type@{j}}.
-  Variable f : T -> U.
+  Polymorphic Context {T : Type@{i}} {U : Type@{j}}.
+  Polymorphic Variable f : T -> U.
 
   Polymorphic Definition fmap_poption (x : poption@{i} T) : poption@{j} U :=
     match x with

theories/Data/PreFun.v

@@ -18,7 +18,7 @@ Section type.
 
   Polymorphic Variables (tOk : typeOk tT) (uOk : typeOk tU).
 
-  Global Instance typeOk_Fun : typeOk type_Fun.
+  Global Polymorphic Instance typeOk_Fun : typeOk type_Fun.
   Proof.
     constructor.
     { unfold equiv. simpl. unfold respectful.
@@ -41,27 +41,27 @@ Section type.
       apply tOk. }
   Qed.
 
-  Global Instance proper_app : forall (f : T -> U) (a : T),
+  Global Polymorphic Instance proper_app : forall (f : T -> U) (a : T),
     proper f -> proper a -> proper (f a).
   Proof.
     simpl; intros. red in H.
     eapply proper_left; eauto.
     eapply H. eapply preflexive. eapply equiv_prefl; auto. auto.
   Qed.
 
-  Theorem proper_fun : forall (f : T -> U),
+  Polymorphic Theorem proper_fun : forall (f : T -> U),
     (forall x y, equal x y -> equal (f x) (f y)) ->
     proper f.
   Proof.
     intros. do 3 red. eauto.
   Qed.
 
-  Theorem equal_fun : forall (f g : T -> U),
+  Polymorphic Theorem equal_fun : forall (f g : T -> U),
     (forall x y, equal x y -> equal (f x) (g y)) ->
     equal f g.
   Proof. intros. do 3 red. apply H. Qed.
 
-  Theorem equal_app : forall (f g : T -> U) (x y : T),
+  Polymorphic Theorem equal_app : forall (f g : T -> U) (x y : T),
     equal f g -> equal x y ->
     equal (f x) (g y).
   Proof.

theories/Structures/Monoid.v

@@ -12,7 +12,7 @@ Section Monoid.
   ; monoid_unit : S
   }.
 
-  Context {Type_S : type S}.
+  Polymorphic Context {Type_S : type S}.
 
   Polymorphic Class MonoidLaws (M : Monoid) : Type :=
   { monoid_assoc :> Associative M.(monoid_plus) equal