Set Polymorphic Inductive Cumulativity

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.
 

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

theories/Data/List.v

@@ -10,6 +10,7 @@ Require Import ExtLib.Tactics.Injection.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Section EqDec.
   Universe u.

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})

theories/Data/PList.v

@@ -9,94 +9,95 @@ 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
     | _ , _ => pNone
     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

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.

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.

theories/Data/PreFun.v

@@ -4,6 +4,7 @@ Require Import Coq.Relations.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.
 

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]

theories/Programming/Show.v

@@ -15,6 +15,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Set Printing Universes.
 

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

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.