working on porting to 8.5 beta 3

Author: Gregory Malecha

_CoqProject

@@ -0,0 +1,127 @@
+-Q theories ExtLib
+
+
+theories/ExtLib.v
+theories/Tactics.v
+
+theories/Core/Any.v
+theories/Core/CmpDec.v
+theories/Core/EquivDec.v
+theories/Core/RelDec.v
+theories/Core/Type.v
+
+theories/Structures/Applicative.v
+theories/Structures/BinOps.v
+theories/Structures/CoFunctor.v
+theories/Structures/CoMonad.v
+theories/Structures/EqDep.v
+theories/Structures/Foldable.v
+theories/Structures/FunctorLaws.v
+theories/Structures/Functor.v
+theories/Structures/Identity.v
+theories/Structures/Maps.v
+theories/Structures/MonadCont.v
+theories/Structures/MonadExc.v
+theories/Structures/MonadFix.v
+theories/Structures/MonadLaws.v
+theories/Structures/MonadPlus.v
+theories/Structures/MonadReader.v
+theories/Structures/MonadState.v
+theories/Structures/Monads.v
+theories/Structures/MonadTrans.v
+theories/Structures/Monad.v
+theories/Structures/MonadWriter.v
+theories/Structures/MonadZero.v
+theories/Structures/Monoid.v
+theories/Structures/Proper.v
+theories/Structures/Reducible.v
+theories/Structures/Sets.v
+theories/Structures/Traversable.v
+
+theories/Data/Bool.v
+theories/Data/Char.v
+theories/Data/Checked.v
+theories/Data/Eq.v
+theories/Data/Fin.v
+theories/Data/Fun.v
+theories/Data/HList.v
+theories/Data/LazyList.v
+theories/Data/Lazy.v
+theories/Data/ListFirstnSkipn.v
+theories/Data/ListNth.v
+theories/Data/List.v
+theories/Data/Member.v
+theories/Data/Nat.v
+theories/Data/N.v
+theories/Data/Option.v
+theories/Data/Pair.v
+theories/Data/Positive.v
+theories/Data/PreFun.v
+theories/Data/Prop.v
+theories/Data/SigT.v
+theories/Data/Stream.v
+theories/Data/String.v
+theories/Data/SumN.v
+theories/Data/Sum.v
+theories/Data/Tuple.v
+theories/Data/Unit.v
+theories/Data/Vector.v
+theories/Data/Z.v
+
+theories/Generic/Data.v
+theories/Generic/DerivingData.v
+theories/Generic/Func.v
+theories/Generic/Ind.v
+
+theories/Programming/Eqv.v
+theories/Programming/Extras.v
+theories/Programming/Injection.v
+theories/Programming/Le.v
+theories/Programming/Show.v
+theories/Programming/With.v
+
+theories/Recur/Facts.v
+theories/Recur/GenRec.v
+theories/Recur/Measure.v
+theories/Recur/Relation.v
+
+theories/Relations/Compose.v
+theories/Relations/TransitiveClosure.v
+
+theories/Tactics/BoolTac.v
+theories/Tactics/Cases.v
+theories/Tactics/Consider.v
+theories/Tactics/EqDep.v
+theories/Tactics/Equality.v
+theories/Tactics/Forward.v
+theories/Tactics/Injection.v
+theories/Tactics/MonadTac.v
+theories/Tactics/Parametric.v
+theories/Tactics/Reify.v
+theories/Tactics/TypeTac.v
+
+theories/Data/Graph/BuildGraph.v
+theories/Data/Graph/GraphAdjList.v
+theories/Data/Graph/GraphAlgos.v
+theories/Data/Graph/Graph.v
+
+theories/Data/Map/FMapAList.v
+theories/Data/Map/FMapPositive.v
+theories/Data/Map/FMapTwoThreeK.v
+
+theories/Data/Monads/ContMonad.v
+theories/Data/Monads/EitherMonad.v
+theories/Data/Monads/FuelMonadLaws.v
+theories/Data/Monads/FuelMonad.v
+theories/Data/Monads/IdentityMonadLaws.v
+theories/Data/Monads/IdentityMonad.v
+theories/Data/Monads/ListMonad.v
+theories/Data/Monads/OptionMonadLaws.v
+theories/Data/Monads/OptionMonad.v
+theories/Data/Monads/ReaderMonadLaws.v
+theories/Data/Monads/ReaderMonad.v
+theories/Data/Monads/StateMonad.v
+theories/Data/Monads/WriterMonad.v
+theories/Data/Set/ListSet.v
+theories/Data/Set/SetMap.v
+theories/Data/Set/TwoThreeTrees.v

theories/Core/Type.v

@@ -5,17 +5,17 @@ Require Import ExtLib.Structures.Proper.
  ** Proper elements are the elements for which the equivalence
  ** relation is reflexive.
  **)
-Polymorphic Class type (T : Type) : Type :=
+Polymorphic Class type@{t} (T : Type@{t}) : Type :=
 { equal : T -> T -> Prop
 ; proper : T -> Prop
 }.
 
-Polymorphic Definition type_from_equal {T} (r : T -> T -> Prop) : type T :=
+Polymorphic Definition type_from_equal@{t} {T : Type@{t}} (r : T -> T -> Prop) : type@{t} T :=
 {| equal := r
  ; proper := fun x => r x x
  |}.
 
-Polymorphic Definition type_libniz T : type T :=
+Polymorphic Definition type_libniz@{t} (T : Type@{t}) : type@{t} T :=
 {| equal := @eq T
  ; proper := fun _ => True
  |}.
@@ -58,23 +58,25 @@ Section type.
 End type.
 
 
-Polymorphic Definition type1 (F : Type@{d} -> Type@{r}) : Type :=
-  forall {T:Type@{d}}, type T -> type (F T).
+Polymorphic Definition type1@{d r z} (F : Type@{d} -> Type@{r}) : Type@{z} :=
+  forall {T:Type@{d}}, type@{d} T -> type@{r} (F T).
 
-Polymorphic Definition type2 (F : Type@{t} -> Type@{u} -> Type@{v}) : Type :=
+Polymorphic Definition type2@{t u v z} (F : Type@{t} -> Type@{u} -> Type@{v}) : Type@{z} :=
   forall {T:Type@{t}}, type T -> forall {U:Type@{u}}, type U -> type (F T U).
 
-Polymorphic Definition type3 (F : Type@{t} -> Type@{u} -> Type@{v} -> Type@{w}) : Type :=
+Polymorphic Definition type3@{t u v w z} (F : Type@{t} -> Type@{u} -> Type@{v} -> Type@{w}) : Type@{z} :=
   forall {T:Type@{t}}, type T -> forall {U:Type@{u}}, type U -> forall {V:Type@{w}}, type V ->  type (F T U V).
 
-Polymorphic Definition typeOk1 F (tF : type1 F) : Type :=
-  forall T tT, @typeOk T tT -> typeOk (tF _ tT).
+Polymorphic Definition typeOk1@{d r z} (F : Type@{d} -> Type@{r}) (tF : type1@{d r z} F) : Type@{z} :=
+  forall (T : Type@{d}) tT, @typeOk T tT -> typeOk (tF _ tT).
 
-Polymorphic Definition typeOk2 F (tF : type2 F) : Type :=
-  forall T tT, @typeOk T tT -> typeOk1 _ (tF _ tT).
+Polymorphic Definition typeOk2@{t u v z}
+            (F : Type@{t} -> Type@{u} -> Type@{v}) (tF : type2@{t u v z} F)
+: Type@{z} :=
+  forall (T : Type@{t}) (tT : type@{t} T), @typeOk@{t} T tT -> typeOk1@{u v z} _ (tF _ tT).
 
-Polymorphic Definition typeOk3 F (tF : type3 F) : Type :=
-  forall T tT, @typeOk T tT -> typeOk2 _ (tF _ tT).
+Polymorphic Definition typeOk3@{t u v w z} F (tF : type3 F) : Type@{z} :=
+  forall (T : Type@{t}) tT, @typeOk@{t} T tT -> typeOk2@{u v w z} _ (tF _ tT).
 
 Existing Class type1.
 Existing Class type2.

theories/Data/PreFun.v

@@ -6,17 +6,17 @@ Require Import ExtLib.Core.Type.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Polymorphic Definition Fun A B := A -> B.
+Polymorphic Definition Fun@{d c} (A : Type@{d}) (B : Type@{c}) := A -> B.
 
 Section type.
-  Polymorphic Variables (T : Type@{t}) (U : Type@{u}) (tT : type T) (tU : type U).
+  Polymorphic Variables (T : Type) (U : Type) (tT : type T) (tU : type U).
 
   Global Polymorphic Instance type_Fun  : type (T -> U) :=
   { equal := fun f g => respectful equal equal f g
   ; proper := fun x => respectful equal equal x x
   }.
 
-  Variables (tOk : typeOk tT) (uOk : typeOk tU).
+  Polymorphic Variables (tOk : typeOk tT) (uOk : typeOk tU).
 
   Global Instance typeOk_Fun : typeOk type_Fun.
   Proof.
@@ -71,4 +71,4 @@ Section type.
 End type.
 
 Polymorphic Definition compose {A:Type} {B:Type} {C : Type} (g : B -> C) (f : A -> B) : A -> C :=
-  fun x => g (f x).
+  fun x => g (f x).

theories/Structures/Applicative.v

@@ -1,13 +1,13 @@
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 
-Polymorphic Class PApplicative (T : Type@{d} -> Type) :=
-{ AppP : Type@{d} -> Type
+Polymorphic Class PApplicative@{d c p} (T : Type@{d} -> Type@{c}) :=
+{ AppP : Type@{d} -> Type@{p}
 ; ppure : forall {A : Type@{d}} {P : AppP A}, A -> T A
 ; pap : forall {A B : Type@{d}} {P : AppP B}, T (A -> B) -> T A -> T B
 }.
 
-Polymorphic Class Applicative (T : Type@{d} -> Type) :=
+Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
 { pure : forall {A : Type@{d}}, A -> T A
 ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
 }.
@@ -18,6 +18,6 @@ End ApplicativeNotation.
 Import ApplicativeNotation.
 
 Section applicative.
-  Polymorphic Definition liftA {T : Type@{d} -> Type} {AT:Applicative T} {A B : Type@{d}} (f:A -> B) (aT:T A) : T B := pure f <*> aT.
-  Polymorphic Definition liftA2 {T : Type@{d} -> Type} {AT:Applicative T} {A B C : Type@{d}} (f:A -> B -> C) (aT:T A) (bT:T B) : T C := liftA f aT <*> bT.
+  Polymorphic Definition liftA@{d c} {T : Type@{d} -> Type@{c}} {AT:Applicative@{d c} T} {A B : Type@{d}} (f:A -> B) (aT:T A) : T B := pure f <*> aT.
+  Polymorphic Definition liftA2@{d c} {T : Type@{d} -> Type@{c}} {AT:Applicative@{d c} T} {A B C : Type@{d}} (f:A -> B -> C) (aT:T A) (bT:T B) : T C := liftA f aT <*> bT.
 End applicative.

theories/Structures/CoFunctor.v

@@ -4,24 +4,21 @@ Set Implicit Arguments.
 Set Strict Implicit.
 
 Section functor.
-  Polymorphic Variable F : Type@{d} -> Type.
 
-  Polymorphic Class CoFunctor : Type :=
+  Polymorphic Class CoFunctor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
   { cofmap : forall {A B : Type@{d}}, (B -> A) -> F A -> F B }.
 
-  Definition ID {T : Type} (f : T -> T) : Prop :=
-    forall x, f x = x.
-
-  Polymorphic Class CoPFunctor : Type :=
-  { CoFunP : Type -> Type
-  ; copfmap : forall {A B} {P : CoFunP B}, (B -> A) -> F A -> F B
+  Polymorphic Class CoPFunctor@{d c p} (F : Type@{d} -> Type@{c}) : Type :=
+  { CoFunP : Type@{d} -> Type@{p}
+  ; copfmap : forall {A B : Type@{d}} {P : CoFunP B}, (B -> A) -> F A -> F B
   }.
 
   Existing Class CoFunP.
   Hint Extern 0 (@CoFunP _ _ _) => progress (simpl CoFunP) : typeclass_instances.
 
-  Global Polymorphic Instance CoPFunctor_From_CoFunctor (F : CoFunctor) : CoPFunctor :=
-  { CoFunP := Any
-  ; copfmap := fun _ _ _ f x => cofmap f x
-  }.
+  Polymorphic Definition CoPFunctor_From_CoFunctor@{d c p} (F : Type@{d} -> Type@{c}) (F_ : CoFunctor@{d c} F) : CoPFunctor@{d c p} F :=
+  {| CoFunP := Any@{p}
+   ; copfmap := fun _ _ _ f x => cofmap f x
+   |}.
+  Global Existing Instance CoPFunctor_From_CoFunctor.
 End functor.

theories/Structures/Functor.v

@@ -3,25 +3,27 @@ Require Import ExtLib.Core.Any.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Polymorphic Class Functor (F : Type@{d} -> Type) : Type :=
+Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
 { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }.
 
-Polymorphic Definition ID {T : Type@{d}} (f : T -> T) : Prop :=
-  forall x, f x = x.
+Polymorphic Definition ID@{d} {T : Type@{d}} (f : T -> T) : Prop :=
+  forall x : T, f x = x.
 
-Polymorphic Class PFunctor (F : Type@{d} -> Type) : Type :=
-{ FunP : Type@{d} -> Type
+Polymorphic Class PFunctor@{d c p} (F : Type@{d} -> Type@{c}) : Type :=
+{ FunP : Type@{d} -> Type@{p}
 ; pfmap : forall {A B : Type@{d}} {P : FunP B}, (A -> B) -> F A -> F B
 }.
 
 Existing Class FunP.
 Hint Extern 0 (@FunP _ _ _) => progress (simpl FunP) : typeclass_instances.
 
-Global Polymorphic Instance PFunctor_From_Functor
-       (F : Type@{d} -> Type) (FunF : Functor F) : PFunctor F :=
-{ FunP := Any
+(** TODO: This is due to a but in current 8.5 **)
+Polymorphic Definition PFunctor_From_Functor@{d c p}
+       (F : Type@{d} -> Type@{c}) (FunF : Functor@{d c} F) : PFunctor@{d c p} F :=
+{| FunP := Any
 ; pfmap := fun _ _ _ f x => fmap f x
-}.
+|}.
+Global Existing Instance PFunctor_From_Functor.
 
 Module FunctorNotation.
   Notation "f <$> x" := (@pfmap _ _ _ _ _ f x) (at level 51, right associativity).

theories/Structures/Monad.v

@@ -5,13 +5,13 @@ Require Import ExtLib.Structures.Applicative.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Polymorphic Class Monad (m : Type@{d} -> Type) : Type :=
+Polymorphic Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 { ret : forall {t : Type@{d}}, t -> m t
 ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
 }.
 
-Polymorphic Class PMonad (m : Type@{d} -> Type) : Type :=
-{ MonP : Type -> Type
+Polymorphic Class PMonad@{d c p} (m : Type@{d} -> Type@{c}) : Type :=
+{ MonP : Type@{d} -> Type@{p}
 ; pret : forall {t : Type@{d}} {Pt : MonP t}, t -> m t
 ; pbind : forall {t u : Type@{d}} {Pu : MonP u}, m t -> (t -> m u) -> m u
 }.
@@ -26,21 +26,31 @@ Global Polymorphic Instance PMonad_Monad m (M : Monad m) : PMonad m :=
 }.
 
 Section monadic.
-  Variable m : Type@{d} -> Type.
-  Context {M : Monad m}.
 
-  Polymorphic Definition liftM {T U : Type@{d}} (f : T -> U) : m T -> m U :=
+  Polymorphic Definition liftM@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U : Type@{d}} (f : T -> U) : m T -> m U :=
     fun x => bind x (fun x => ret (f x)).
 
-  Polymorphic Definition liftM2 {T U V : Type@{d}} (f : T -> U -> V) : m T -> m U -> m V :=
+  Polymorphic Definition liftM2@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U V : Type@{d}} (f : T -> U -> V) : m T -> m U -> m V :=
     Eval cbv beta iota zeta delta [ liftM ] in
       fun x y => bind x (fun x => liftM (f x) y).
 
-  Polymorphic Definition liftM3 {T U V W : Type@{d}} (f : T -> U -> V -> W) : m T -> m U -> m V -> m W :=
+  Polymorphic Definition liftM3@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U V W : Type@{d}} (f : T -> U -> V -> W) : m T -> m U -> m V -> m W :=
     Eval cbv beta iota zeta delta [ liftM2 ] in
       fun x y z => bind x (fun x => liftM2 (f x) y z).
 
-  Polymorphic Definition apM {A B : Type@{d}} (fM:m (A -> B)) (aM:m A) : m B :=
+  Polymorphic Definition apM@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {A B : Type@{d}} (fM:m (A -> B)) (aM:m A) : m B :=
     bind fM (fun f => liftM f aM).
 End monadic.