porting of most things so that it builds with 8.5~beta3

Author: Gregory Malecha

examples/MonadReasoning.v

@@ -7,6 +7,9 @@ Require Import ExtLib.Data.Fun.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** Currently not ported due to universes *)
+
+(*
 Section with_m.
   Variable m : Type -> Type.
   Variable Monad_m : Monad m.
@@ -53,4 +56,5 @@ Section with_m.
       eapply equiv_prefl; eauto. }
   Qed.
 
-End with_m.
+End with_m.
+*)

theories/Data/HList.v

@@ -15,10 +15,10 @@ Set Asymmetric Patterns.
 
 (** Core Type and Functions **)
 Section hlist.
-  Context {iT : Type@{i}}.
-  Variable F : iT -> Type@{d}.
+  Context {iT : Type}.
+  Variable F : iT -> Type.
 
-  Inductive hlist : list iT -> Type@{d} :=
+  Inductive hlist : list iT -> Type :=
   | Hnil  : hlist nil
   | Hcons : forall l ls, F l -> hlist ls -> hlist (l :: ls).
 
@@ -332,7 +332,7 @@ Section hlist.
     end.
 
   Polymorphic Fixpoint hlist_nth ls (h : hlist ls) (n : nat) :
-    match nth_error ls n return Type@{i} with
+    match nth_error ls n return Type with
       | None => unit
       | Some t => F t
     end :=
@@ -398,10 +398,10 @@ Section hlist.
 
   Theorem hlist_nth_hlist_app
   : forall l l' (h : hlist l) (h' : hlist l') n,
-    hlist_nth@{i} (hlist_app h h') n =
+    hlist_nth (hlist_app h h') n =
     match nth_error l n as k
       return nth_error l n = k ->
-      match nth_error (l ++ l') n return Type@{i} with
+      match nth_error (l ++ l') n return Type with
         | None => unit
         | Some t => F t
       end
@@ -410,17 +410,17 @@ Section hlist.
         match
           cast1 _ _ _ pf in _ = z ,
           eq_sym pf in _ = w
-          return match w return Type@{i} with
+          return match w return Type with
                    | None => unit
                    | Some t => F t
                  end ->
-                 match z return Type@{i} with
+                 match z return Type with
                    | None => unit
                    | Some t => F t
                  end
         with
           | eq_refl , eq_refl => fun x => x
-        end (hlist_nth@{i} h n)
+        end (hlist_nth h n)
       | None => fun pf =>
         match cast2 _ _ _ pf in _ = z
           return match z with
@@ -471,7 +471,8 @@ Section hlist.
       { intro. induction ls; simpl.
         { rewrite (hlist_eta x); intros; constructor. }
         { rewrite (hlist_eta x); intros; intuition; constructor.
-          eapply preflexive; eauto with typeclass_instances.
+          eapply preflexive; [ | eauto with typeclass_instances ].
+          eauto with typeclass_instances.
           eapply IHls; eauto. } }
       { red. induction 1.
         { constructor. }
@@ -628,10 +629,10 @@ Section hlist.
 
   Theorem nth_error_get_hlist_nth_Some
     : forall ls n s,
-      nth_error_get_hlist_nth@{i} ls n = Some s ->
+      nth_error_get_hlist_nth ls n = Some s ->
       exists pf : nth_error ls n = Some (projT1 s),
       forall h, projT2 s h = match pf in _ = t
-                                   return match t return Type@{i} with
+                                   return match t return Type with
                                             | Some t => F t
                                             | None => unit
                                           end

theories/Data/Monads/FuelMonadLaws.v

@@ -13,6 +13,7 @@ Require Import ExtLib.Tactics.TypeTac.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section Laws.
   Section fixResult_T.
     Context {T : Type} (e : type T).
@@ -145,3 +146,4 @@ Section Laws.
 *)
 
 End Laws.
+*)

theories/Data/Monads/IdentityMonadLaws.v

@@ -10,6 +10,7 @@ Require Import ExtLib.Data.Monads.IdentityMonad.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section with_T.
   Context {T : Type} (e : type T).
 
@@ -62,3 +63,4 @@ Proof.
   { simpl; intros. red. solve_equal. }
   { unfold bind, Monad_ident. do 6 red; intros. solve_equal. }
 Qed.
+*)

theories/Data/Monads/OptionMonadLaws.v

@@ -12,6 +12,7 @@ Require Import ExtLib.Tactics.TypeTac.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section Laws.
   Variable m : Type -> Type.
   Variable Monad_m : Monad m.
@@ -294,3 +295,4 @@ setoid_rewrite bind_of_return.
   Qed.
 
 End Laws.
+*)

theories/Data/Monads/ReaderMonadLaws.v

@@ -11,6 +11,7 @@ Require Import ExtLib.Tactics.TypeTac.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section Laws.
   Variable m : Type -> Type.
   Variable Monad_m : Monad m.
@@ -93,3 +94,4 @@ Section Laws.
 *)
 
 End Laws.
+*)

theories/Data/SigT.v

@@ -7,6 +7,7 @@ Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
+Set Printing Universes.
 
 Section type.
   Variable T : Type.
@@ -32,12 +33,14 @@ Section type.
   Proof.
     constructor.
     { destruct x; destruct y; intros. simpl in *. destruct H. destruct H0. subst.
-      apply only_proper in H; eauto with typeclass_instances.
-      apply only_proper in H0; eauto with typeclass_instances. intuition. }
+      apply only_proper in H; [ | eauto with typeclass_instances ].
+      apply only_proper in H0; [ | eauto with typeclass_instances ]. intuition. }
     { red. destruct x; intros. do 2 red in H.
       do 2 red; simpl in *. intuition.
       try solve [ apply equiv_prefl; eauto ].
-      exists eq_refl. solve_equal. }
+      exists eq_refl.
+      eapply Proper.preflexive; [ | eapply H1 ].
+      eauto with typeclass_instances. }
     { red; destruct x; destruct y; intros; simpl in *.
       intuition. destruct H1; subst. exists eq_refl. symmetry; assumption. }
     { red; destruct x; destruct y; destruct z; intros; simpl in *; intuition.

theories/Generic/DerivingData.v

@@ -15,9 +15,9 @@ Fixpoint dataD (T : Type) (X : T -> Type) (d : data X) : Type :=
   match d with
     | Inj _X x => x
     | Get X i => X i
-    | Prod X l r => prod (dataD l) (dataD r)
-    | Sigma X i s => @sigT i (fun v => dataD (s v))
-    | Pi X i s => forall v : i, dataD (s v)
+    | Prod l r => prod (dataD l) (dataD r)
+    | @Sigma _ _ i s => @sigT i (fun v => dataD (s v))
+    | @Pi _ _ i s => forall v : i, dataD (s v)
   end.
 
 (** Example of lists as data **)
@@ -46,29 +46,30 @@ Fixpoint dataP (T : Type) (X : T -> Type) (d : data X) (R : Type) : Type :=
   match d with
     | Inj _X x => x -> R
     | Get X x => X x -> R
-    | Prod X l r => dataP l (dataP r R)
-    | Sigma X i s => forall i, dataP (s i) R
-    | Pi X i s => (forall i, dataD (s i)) -> R
+    | @Prod _ _ l r => dataP l (dataP r R)
+    | @Sigma _ _ i s => forall i, dataP (s i) R
+    | @Pi _ _ i s => (forall i, dataD (s i)) -> R
   end.
 
 Fixpoint dataMatch (T : Type) (X : T -> Type) (d : data X) {struct d} 
   : forall (R : Type), dataP d R -> dataD d -> R :=
     match d as d return forall (R : Type), dataP d R -> dataD d -> R with
       | Inj _ _ => fun _ p => p
       | Get X x => fun _ p => p
-      | Prod X l r => fun _ p v => 
+      | @Prod _ _ l r => fun _ p v => 
         dataMatch r _ (dataMatch l _ p (fst v)) (snd v)
-      | Sigma X i d => fun _ p v => 
+      | @Sigma _ _ i d => fun _ p v => 
         match v with
-          | existT x y => dataMatch (d x) _ (p _) y
+        | existT _ x y => dataMatch (d x) _ (p _) y
         end
-      | Pi X i d => fun _ p v => p v
+      | @Pi _ _ i d => fun _ p v => p v
     end.
 
-
+(* This used to work
 (** You really need a fold! **)
-Fixpoint dataLength {x} (l : list x) : nat :=
+Fixpoint dataLength {x} (l : list x) Z {struct l} : nat :=
   dataMatch (dataList x) _ (fun tag => match tag with
-                                         | true => fun _ => 0
-                                         | false => fun h t => S (dataLength t)
+                                       | true => fun _ => 0
+                                       | false => fun h t => S (Z t) (* (dataLength t) *)
                                        end) (list_to_dataList l).
+*)

theories/Programming/Show.v

@@ -15,11 +15,13 @@ Set Strict Implicit.
 
 Set Printing Universes.
 
-Polymorphic Definition showM : Type :=
-  forall m : Type, Injection ascii m -> Monoid m -> m.
+Universe Ushow.
 
-Polymorphic Class ShowScheme (T : Type) : Type :=
-{ show_mon : Monoid T
+Polymorphic Definition showM@{T} : Type@{Ushow} :=
+  forall m : Type@{T}, Injection ascii m -> Monoid m -> m.
+
+Polymorphic Class ShowScheme@{t} (T : Type@{t}) : Type :=
+{ show_mon : Monoid@{t} T
 ; show_inj : Injection ascii T
 }.
 
@@ -36,7 +38,8 @@ Global Instance ShowScheme_string_compose : ShowScheme (string -> string) :=
 Polymorphic Definition runShow {T} {M : ShowScheme T} (m : showM) : T :=
   m _ show_inj show_mon.
 
-Polymorphic Class Show T := show : T -> showM.
+Polymorphic Class Show@{t m} (T : Type@{t}) : Type :=
+  show : T -> showM@{m}.
 
 Polymorphic Definition to_string {T} {M : Show T} (v : T) : string :=
   runShow (show v) ""%string.
@@ -73,10 +76,9 @@ Polymorphic Definition indent (indent : showM) (v : showM) : showM :=
 Section sepBy.
   Import ShowNotation.
   Local Open Scope show_scope.
-  Polymorphic Variable T : Type.
-  Context {F : Foldable T showM}.
 
-  Polymorphic Definition sepBy (sep : showM) (ls : T) : showM :=
+  Polymorphic Definition sepBy {T : Type}
+              {F : Foldable T showM} (sep : showM) (ls : T) : showM :=
     match
       fold (fun s acc =>
         match acc with
@@ -115,9 +117,11 @@ Polymorphic Definition wrap (before after : showM) (x : showM) : showM :=
 Section sum_Show.
   Import ShowNotation.
   Local Open Scope show_scope.
-  Polymorphic Context {A : Type@{a}} {B : Type@{b}} {AS:Show A} {BS:Show B}.
-  Global Polymorphic Instance sum_Show : Show (A+B) :=
-    { show s :=
+
+  Polymorphic Definition sum_Show@{a m}
+              {A : Type@{a}} {B : Type@{a}} {AS:Show@{a m} A} {BS:Show@{a m} B}
+  : Show@{a m} (A+B) :=
+    fun s =>
         let (tag, payload) :=
           match s with
           | inl a => (show_exact "inl"%string, show a)
@@ -128,8 +132,8 @@ Section sum_Show.
         tag <<
         " "%char <<
         payload <<
-        ")"%char
-    }.
+        ")"%char.
+        
 End sum_Show.
 
 Section foldable_Show.
@@ -188,12 +192,12 @@ Global Instance Show_Z : Show Z :=
     end.
 
 Section pair_Show.
-  Polymorphic Context {A : Type@{a}} {B : Type@{b}} {AS:Show A} {BS:Show B}.
-  Global Polymorphic Instance pair_Show : Show (A*B) :=
-    { show p :=
-        let (a,b) := p in
-        "("%char << show a << ","%char << show b << ")"%char
-    }.
+  Polymorphic Definition pair_Show@{a m}
+              {A : Type@{a}} {B : Type@{a}} {AS:Show A} {BS:Show B}
+  : Show (A*B) :=
+    fun p =>
+      let (a,b) := p in
+      "("%char << show a << ","%char << show b << ")"%char.
 End pair_Show.
 End hiding_notation.
 

theories/Structures/FunctorLaws.v

@@ -10,22 +10,23 @@ Set Strict Implicit.
 
 Section laws.
 
-  Polymorphic Class FunctorLaws
+  Polymorphic Class FunctorLaws@{t u X}
               (F : Type@{t} -> Type@{u})
               (Functor_F : Functor F)
-              (Feq : type1 F)
+              (Feq : type1@{t u X} F)
   : Type :=
-  { fmap_id : forall T (tT : type T),
-      typeOk tT -> forall (f : T -> T),
+  { fmap_id : forall (T : Type@{t}) (tT : type@{t} T)
+      (tTo : typeOk@{t} tT) (f : T -> T),
         IsIdent f ->
         equal (fmap f) (@id (F T))
-  ; fmap_compose : forall T U V (tT : type T) (tU : type U) (tV : type V),
+  ; fmap_compose : forall (T U V : Type@{t})
+                          (tT : type@{t} T) (tU : type@{t} U) (tV : type@{t} V),
       typeOk tT -> typeOk tU -> typeOk tV ->
       forall (f : T -> U) (g : U -> V),
         proper f -> proper g ->
         equal (fmap (compose g f)) (compose (fmap g) (fmap f))
-  ; fmap_proper :> forall T U (tT : type T) (tU : type U),
-      typeOk tT -> typeOk tU ->
+  ; fmap_proper :> forall (T : Type@{t}) (U : Type@{u}) (tT : type T) (tU : type U),
+      typeOk@{t} tT -> typeOk@{u} tU ->
       proper (@fmap _ _ T U)
   }.
 End laws.