diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index ee71ea1..b7fb7db 100644
--- a/theories/Core/Any.v
+++ b/theories/Core/Any.v
@@ -1,12 +1,14 @@
 Set Implicit Arguments.
 Set Strict Implicit.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 (** This class should be used when no requirements are needed **)
-Polymorphic Class Any (T : Type) : Prop.
+Class Any (T : Type) : Type.
 
-Global Polymorphic Instance Any_a (T : Type) : Any T := {}.
+Global Instance Any_a (T : Type) : Any T := {}.
 
-Polymorphic Definition RESOLVE (T : Type) : Type := T.
+Definition RESOLVE (T : Type) : Type := T.
 
 Existing Class RESOLVE.
 
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index d075703..6709175 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -12,6 +12,7 @@ Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Lemma app_ass_trans@{X}
@@ -35,7 +36,7 @@ Monomorphic Universe hlist_large.
 
 (** Core Type and Functions **)
 Section hlist.
-  Polymorphic Universe Ui Uv.
+  Universe Ui Uv.
 
   Context {iT : Type@{Ui}}.
   Variable F : iT -> Type@{Uv}.
@@ -342,7 +343,7 @@ Section hlist.
         end
     end.
 
-  Polymorphic Fixpoint hlist_nth ls (h : hlist ls) (n : nat) :
+  Fixpoint hlist_nth ls (h : hlist ls) (n : nat) :
     match nth_error ls n return Type with
       | None => unit
       | Some t => F t
@@ -561,7 +562,7 @@ Section hlist.
     rewrite Heqp. reflexivity.
   Qed.
 
-  Polymorphic Fixpoint nth_error_get_hlist_nth (ls : list iT) (n : nat) {struct ls} :
+  Fixpoint nth_error_get_hlist_nth (ls : list iT) (n : nat) {struct ls} :
     option {t : iT & hlist ls -> F t} :=
     match
       ls as ls0
diff --git a/theories/Data/List.v b/theories/Data/List.v
index f76c7fd..b515c38 100644
--- a/theories/Data/List.v
+++ b/theories/Data/List.v
@@ -9,6 +9,7 @@ Require Import ExtLib.Tactics.Injection.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section EqDec.
   Universe u.
diff --git a/theories/Data/Monads/WriterMonad.v b/theories/Data/Monads/WriterMonad.v
index f3c1dc2..0ac8520 100644
--- a/theories/Data/Monads/WriterMonad.v
+++ b/theories/Data/Monads/WriterMonad.v
@@ -8,11 +8,12 @@ Require Import Coq.Program.Basics. (* for (∘) *)
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Set Printing Universes.
 
 Section WriterType.
-  Polymorphic Universe s d c.
+  Universe s d c.
   Variable S : Type@{s}.
 
   Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c})
diff --git a/theories/Data/PList.v b/theories/Data/PList.v
index d8b9ff1..0682018 100644
--- a/theories/Data/PList.v
+++ b/theories/Data/PList.v
@@ -9,76 +9,77 @@ Require Import ExtLib.Tactics.Injection.
 Require Import Coq.Bool.Bool.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Primitive Projections.
 
 Section plist.
-  Polymorphic Universe i.
+  Universe i.
   Variable T : Type@{i}.
 
-  Polymorphic Inductive plist : Type@{i} :=
+  Inductive plist : Type@{i} :=
   | pnil
   | pcons : T -> plist -> plist.
 
-  Polymorphic Fixpoint length (ls : plist) : nat :=
+  Fixpoint length (ls : plist) : nat :=
     match ls with
     | pnil => 0
     | pcons _ ls' => S (length ls')
     end.
 
-  Polymorphic Fixpoint app (ls ls' : plist) : plist :=
+  Fixpoint app (ls ls' : plist) : plist :=
     match ls with
     | pnil => ls'
     | pcons l ls => pcons l (app ls ls')
     end.
 
-  Polymorphic Definition hd (ls : plist) : poption T :=
+  Definition hd (ls : plist) : poption T :=
     match ls with
     | pnil => pNone
     | pcons x _ => pSome x
     end.
 
-  Polymorphic Definition tl (ls : plist) : plist :=
+  Definition tl (ls : plist) : plist :=
     match ls with
     | pnil => ls
     | pcons _ ls => ls
     end.
 
-  Polymorphic Fixpoint pIn (a : T) (l : plist) : Prop :=
+  Fixpoint pIn (a : T) (l : plist) : Prop :=
     match l with
     | pnil => False
     | pcons b m => b = a \/ pIn a m
     end.
 
-  Polymorphic Inductive pNoDup : plist -> Prop :=
+  Inductive pNoDup : plist -> Prop :=
     pNoDup_nil : pNoDup pnil
   | pNoDup_cons : forall (x : T) (l : plist),
                  ~ pIn x l -> pNoDup l -> pNoDup (pcons x l).
 
-  Polymorphic Fixpoint inb {RelDecA : RelDec (@eq T)} (x : T) (lst : plist) :=
+  Fixpoint inb {RelDecA : RelDec (@eq T)} (x : T) (lst : plist) :=
     match lst with
     | pnil => false
     | pcons l ls => if x ?[ eq ] l then true else inb x ls
     end.
 
-  Polymorphic Fixpoint anyb (p : T -> bool) (ls : plist) : bool :=
+  Fixpoint anyb (p : T -> bool) (ls : plist) : bool :=
     match ls with
     | pnil => false
     | pcons l ls0 => if p l then true else anyb p ls0
     end.
 
-  Polymorphic Fixpoint allb (p : T -> bool) (lst : plist) : bool :=
+  Fixpoint allb (p : T -> bool) (lst : plist) : bool :=
     match lst with
     | pnil => true
     | pcons l ls => if p l then allb p ls else false
     end.
 
-  Polymorphic Fixpoint nodup {RelDecA : RelDec (@eq T)} (lst : plist) :=
+  Fixpoint nodup {RelDecA : RelDec (@eq T)} (lst : plist) :=
     match lst with
     | pnil => true
     | pcons l ls => andb (negb (inb l ls)) (nodup ls)
     end.
 
-  Polymorphic Fixpoint nth_error (ls : plist) (n : nat) : poption T :=
+  Fixpoint nth_error (ls : plist) (n : nat) : poption T :=
     match n , ls with
     | 0 , pcons l _ => pSome l
     | S n , pcons _ ls => nth_error ls n
@@ -86,17 +87,17 @@ Section plist.
     end.
 
   Section folds.
-    Polymorphic Universe j.
+    Universe j.
     Context {U : Type@{j}}.
     Variable f : T -> U -> U.
 
-    Polymorphic Fixpoint fold_left (acc : U) (ls : plist) : U :=
+    Fixpoint fold_left (acc : U) (ls : plist) : U :=
       match ls with
       | pnil => acc
       | pcons l ls => fold_left (f l acc) ls
       end.
 
-    Polymorphic Fixpoint fold_right (ls : plist) (rr : U) : U :=
+    Fixpoint fold_right (ls : plist) (rr : U) : U :=
       match ls with
       | pnil => rr
       | pcons l ls => f l (fold_right ls rr)
@@ -120,7 +121,7 @@ Arguments nth_error {_} _ _.
 
 
 Section plistFun.
-  Polymorphic Fixpoint split {A B : Type} (lst : plist (pprod A B)) :=
+  Fixpoint split {A B : Type} (lst : plist (pprod A B)) :=
     match lst with
     | pnil => (pnil, pnil)
     | pcons (ppair x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
@@ -202,29 +203,29 @@ Section plistOk.
 End plistOk.
 
 Section pmap.
-  Polymorphic Universe i j.
+  Universe i j.
   Context {T : Type@{i}}.
   Context {U : Type@{j}}.
   Variable f : T -> U.
 
-  Polymorphic Fixpoint fmap_plist (ls : plist@{i} T) : plist@{j} U :=
+  Fixpoint fmap_plist (ls : plist@{i} T) : plist@{j} U :=
     match ls with
     | pnil => pnil
     | pcons l ls => pcons (f l) (fmap_plist ls)
     end.
 End pmap.
 
-Polymorphic Definition Functor_plist@{i} : Functor@{i i} plist@{i} :=
+Definition Functor_plist@{i} : Functor@{i i} plist@{i} :=
 {| fmap := @fmap_plist@{i i} |}.
 #[global]
 Existing Instance Functor_plist.
 
 
 Section applicative.
-  Polymorphic Universe i j.
+  Universe i j.
 
   Context {T : Type@{i}} {U : Type@{j}}.
-  Polymorphic Fixpoint ap_plist
+  Fixpoint ap_plist
               (fs : plist@{i} (T -> U)) (xs : plist@{i} T)
     : plist@{j} U :=
     match fs with
@@ -233,17 +234,17 @@ Section applicative.
     end.
 End applicative.
 
-Polymorphic Definition Applicative_plist@{i} : Applicative@{i i} plist@{i} :=
+Definition Applicative_plist@{i} : Applicative@{i i} plist@{i} :=
 {| pure := fun _ val => pcons val pnil
  ; ap := @ap_plist
  |}.
 
 Section PListEq.
-  Polymorphic Universe i.
+  Universe i.
   Variable T : Type@{i}.
   Variable EDT : RelDec (@eq T).
 
-  Polymorphic Fixpoint plist_eqb (ls rs : plist T) : bool :=
+  Fixpoint plist_eqb (ls rs : plist T) : bool :=
     match ls , rs with
       | pnil , pnil => true
       | pcons l ls , pcons r rs =>
@@ -252,12 +253,12 @@ Section PListEq.
     end.
 
   (** Specialization for equality **)
-  Global Polymorphic Instance RelDec_eq_plist : RelDec (@eq (plist T)) :=
+  Global Instance RelDec_eq_plist : RelDec (@eq (plist T)) :=
   { rel_dec := plist_eqb }.
 
   Variable EDCT : RelDec_Correct EDT.
 
-  Global Polymorphic Instance RelDec_Correct_eq_plist : RelDec_Correct RelDec_eq_plist.
+  Global Instance RelDec_Correct_eq_plist : RelDec_Correct RelDec_eq_plist.
   Proof.
     constructor; induction x; destruct y; split; simpl in *; intros;
       repeat match goal with
diff --git a/theories/Data/POption.v b/theories/Data/POption.v
index ce2de98..40e2b16 100644
--- a/theories/Data/POption.v
+++ b/theories/Data/POption.v
@@ -3,6 +3,7 @@ Require Import ExtLib.Structures.Applicative.
 Require Import ExtLib.Tactics.Injection.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Section poption.
diff --git a/theories/Data/PPair.v b/theories/Data/PPair.v
index 2177e39..953e67f 100644
--- a/theories/Data/PPair.v
+++ b/theories/Data/PPair.v
@@ -4,12 +4,13 @@ Require Import ExtLib.Tactics.Injection.
 Set Printing Universes.
 Set Primitive Projections.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section pair.
-  Polymorphic Universes i j.
+  Universes i j.
   Variable (T : Type@{i}) (U : Type@{j}).
 
-  Polymorphic Record pprod : Type@{max (i, j)} := ppair
+  Record pprod : Type@{max (i, j)} := ppair
   { pfst : T
   ; psnd : U }.
 
@@ -20,7 +21,7 @@ Arguments ppair {_ _} _ _.
 Arguments pfst {_ _} _.
 Arguments psnd {_ _} _.
 
-  Polymorphic Lemma eq_pair_rw
+  Lemma eq_pair_rw
   : forall T U (a b : T) (c d : U) (pf : (ppair a c) = (ppair b d)),
     exists (pf' : a = b) (pf'' : c = d),
       pf = match pf' , pf'' with
@@ -49,7 +50,7 @@ Arguments psnd {_ _} _.
   Defined.
 
 Section Injective.
-  Polymorphic Universes i j.
+  Universes i j.
   Context {T : Type@{i}} {U : Type@{j}}.
 
   Global Instance Injective_pprod (a : T) (b : U) c d
@@ -64,21 +65,21 @@ Section Injective.
 End Injective.
 
 Section PProdEq.
-  Polymorphic Universes i j.
+  Universes i j.
   Context {T : Type@{i}} {U : Type@{j}}.
   Context {EDT : RelDec (@eq T)}.
   Context {EDU : RelDec (@eq U)}.
   Context {EDCT : RelDec_Correct EDT}.
   Context {EDCU : RelDec_Correct EDU}.
 
-  Polymorphic Definition ppair_eqb (p1 p2 : pprod T U) : bool :=
+  Definition ppair_eqb (p1 p2 : pprod T U) : bool :=
     pfst p1 ?[ eq ] pfst p2 && psnd p1 ?[ eq ] psnd p2.
 
   (** Specialization for equality **)
-  Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@pprod T U)) :=
+  Global Instance RelDec_eq_ppair : RelDec (@eq (@pprod T U)) :=
   { rel_dec := ppair_eqb }.
 
-  Global Polymorphic Instance RelDec_Correct_eq_ppair
+  Global Instance RelDec_Correct_eq_ppair
   : RelDec_Correct RelDec_eq_ppair.
   Proof.
     constructor. intros p1 p2. destruct p1, p2. simpl.
diff --git a/theories/Data/PreFun.v b/theories/Data/PreFun.v
index 7a26f52..ea3cf92 100644
--- a/theories/Data/PreFun.v
+++ b/theories/Data/PreFun.v
@@ -4,6 +4,7 @@ From Coq.Relations Require Import Relations.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Definition Fun@{d c} (A : Type@{d}) (B : Type@{c}) := A -> B.
 
diff --git a/theories/Programming/Injection.v b/theories/Programming/Injection.v
index 14747c0..26a4d37 100644
--- a/theories/Programming/Injection.v
+++ b/theories/Programming/Injection.v
@@ -3,14 +3,16 @@ Require Import Coq.Strings.String.
 
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
-Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
+Class Injection (x : Type) (t : Type) := inject : x -> t.
 (*
 Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
 *)
 
 #[global]
-Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
+Instance Injection_refl {T : Type} : Injection T T :=
 { inject := @id T }.
 
 #[global]
diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
index e19f4bf..66f4e42 100644
--- a/theories/Programming/Show.v
+++ b/theories/Programming/Show.v
@@ -14,6 +14,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Set Printing Universes.
 
diff --git a/theories/Structures/Applicative.v b/theories/Structures/Applicative.v
index 7a9ba3f..de5b833 100644
--- a/theories/Structures/Applicative.v
+++ b/theories/Structures/Applicative.v
@@ -4,6 +4,7 @@ From ExtLib Require Import
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
 { pure : forall {A : Type@{d}}, A -> T A
diff --git a/theories/Structures/CoFunctor.v b/theories/Structures/CoFunctor.v
index 1095764..d709d9d 100644
--- a/theories/Structures/CoFunctor.v
+++ b/theories/Structures/CoFunctor.v
@@ -3,6 +3,7 @@ Require Import ExtLib.Core.Any.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section functor.
 
diff --git a/theories/Structures/Functor.v b/theories/Structures/Functor.v
index 4ac3a76..217e64a 100644
--- a/theories/Structures/Functor.v
+++ b/theories/Structures/Functor.v
@@ -2,13 +2,15 @@ Require Import ExtLib.Core.Any.
 
 Set Implicit Arguments.
 Set Strict Implicit.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
-Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
+Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
 { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }.
 
 Global Hint Mode Functor ! : typeclass_instances.
 
-Polymorphic Definition ID@{d} {T : Type@{d}} (f : T -> T) : Prop :=
+Definition ID@{d} {T : Type@{d}} (f : T -> T) : Prop :=
   forall x : T, f x = x.
 
 Module FunctorNotation.
diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
index f706fd6..668bf54 100644
--- a/theories/Structures/FunctorLaws.v
+++ b/theories/Structures/FunctorLaws.v
@@ -5,6 +5,7 @@ Require Import ExtLib.Structures.Functor.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section laws.
 
diff --git a/theories/Structures/Monad.v b/theories/Structures/Monad.v
index 695d432..b5fd443 100644
--- a/theories/Structures/Monad.v
+++ b/theories/Structures/Monad.v
@@ -4,6 +4,7 @@ Require Import ExtLib.Structures.Applicative.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 { ret : forall {t : Type@{d}}, t -> m t
diff --git a/theories/Structures/MonadReader.v b/theories/Structures/MonadReader.v
index 4432ca3..68d59f7 100644
--- a/theories/Structures/MonadReader.v
+++ b/theories/Structures/MonadReader.v
@@ -3,6 +3,7 @@
 Require Import ExtLib.Structures.Monad.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Class MonadReader@{d c} (T : Type@{d}) (m : Type@{d} -> Type@{c})
diff --git a/theories/Structures/MonadState.v b/theories/Structures/MonadState.v
index a8eae78..6c5213a 100644
--- a/theories/Structures/MonadState.v
+++ b/theories/Structures/MonadState.v
@@ -1,6 +1,7 @@
 Require Import ExtLib.Structures.Monad.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Class MonadState@{s d c} (T : Type@{s}) (m : Type@{d} -> Type@{c}) : Type :=
diff --git a/theories/Structures/MonadWriter.v b/theories/Structures/MonadWriter.v
index 1e6d017..b65a388 100644
--- a/theories/Structures/MonadWriter.v
+++ b/theories/Structures/MonadWriter.v
@@ -2,6 +2,7 @@ Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.Monoid.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Class MonadWriter@{d c s} (T : Type@{s}) (M : Monoid T)
diff --git a/theories/Structures/Monoid.v b/theories/Structures/Monoid.v
index 4cc7ac2..7755c0c 100644
--- a/theories/Structures/Monoid.v
+++ b/theories/Structures/Monoid.v
@@ -3,6 +3,7 @@ Require Import ExtLib.Structures.BinOps.
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section Monoid.
   Universe u.
diff --git a/theories/Structures/Traversable.v b/theories/Structures/Traversable.v
index eb59141..a915368 100644
--- a/theories/Structures/Traversable.v
+++ b/theories/Structures/Traversable.v
@@ -2,20 +2,22 @@ Require Import ExtLib.Structures.Applicative.
 
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
-Polymorphic Class Traversable@{d r} (T : Type@{d} -> Type@{r}) : Type :=
+Class Traversable@{d r} (T : Type@{d} -> Type@{r}) : Type :=
 { mapT : forall {F : Type@{d} -> Type@{r} }
                 {Ap:Applicative@{d r} F} {A B : Type@{d}},
     (A -> F B) -> T A -> F (T B)
 }.
 
-Polymorphic Definition sequence@{d r}
+Definition sequence@{d r}
             {T : Type@{d} -> Type@{r}}
             {Tr:Traversable T}
             {F : Type@{d} -> Type@{r}} {Ap:Applicative F} {A : Type@{d}}
   : T (F A) -> F (T A) := mapT (@id (F A)).
 
-Polymorphic Definition forT@{d r}
+Definition forT@{d r}
             {T : Type@{d} -> Type@{r}}
             {Tr:Traversable T} {F : Type@{d} -> Type@{r}} {Ap:Applicative F}
             {A B : Type@{d}} (aT:T A) (f:A -> F B) : F (T B)