From 9588b93ce29e88ea8951b4077fa0452332676340 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@cs.harvard.edu>
Date: Sun, 8 Nov 2015 20:51:21 -0800
Subject: [PATCH] porting of most things so that it builds with 8.5~beta3

---
 examples/MonadReasoning.v                |  6 +++-
 theories/Data/HList.v                    | 25 +++++++-------
 theories/Data/Monads/FuelMonadLaws.v     |  2 ++
 theories/Data/Monads/IdentityMonadLaws.v |  2 ++
 theories/Data/Monads/OptionMonadLaws.v   |  2 ++
 theories/Data/Monads/ReaderMonadLaws.v   |  2 ++
 theories/Data/SigT.v                     |  9 +++--
 theories/Generic/DerivingData.v          | 29 ++++++++--------
 theories/Programming/Show.v              | 42 +++++++++++++-----------
 theories/Structures/FunctorLaws.v        | 15 +++++----
 theories/Structures/Identity.v           | 32 ++++++++++--------
 theories/Structures/MonadLaws.v          |  2 ++
 theories/Structures/MonadWriter.v        | 32 ++++++++++--------
 theories/Structures/Traversable.v        | 22 +++++++++----
 theories/Tactics/MonadTac.v              |  2 ++
 15 files changed, 133 insertions(+), 91 deletions(-)

diff --git a/examples/MonadReasoning.v b/examples/MonadReasoning.v
index 7b07af6d..94c2eece 100644
--- a/examples/MonadReasoning.v
+++ b/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.
\ No newline at end of file
+End with_m.
+*)
\ No newline at end of file
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index fef33e1e..06f4eb0b 100644
--- a/theories/Data/HList.v
+++ b/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
diff --git a/theories/Data/Monads/FuelMonadLaws.v b/theories/Data/Monads/FuelMonadLaws.v
index a9d321ee..df6989e9 100644
--- a/theories/Data/Monads/FuelMonadLaws.v
+++ b/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.
+*)
\ No newline at end of file
diff --git a/theories/Data/Monads/IdentityMonadLaws.v b/theories/Data/Monads/IdentityMonadLaws.v
index 6a7be121..1280cd08 100644
--- a/theories/Data/Monads/IdentityMonadLaws.v
+++ b/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.
+*)
\ No newline at end of file
diff --git a/theories/Data/Monads/OptionMonadLaws.v b/theories/Data/Monads/OptionMonadLaws.v
index 39f36f56..7084b7ad 100644
--- a/theories/Data/Monads/OptionMonadLaws.v
+++ b/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.
+*)
\ No newline at end of file
diff --git a/theories/Data/Monads/ReaderMonadLaws.v b/theories/Data/Monads/ReaderMonadLaws.v
index 01bc4c24..8fc126cd 100644
--- a/theories/Data/Monads/ReaderMonadLaws.v
+++ b/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.
+*)
\ No newline at end of file
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index 8e98eb2b..332344a4 100644
--- a/theories/Data/SigT.v
+++ b/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.
diff --git a/theories/Generic/DerivingData.v b/theories/Generic/DerivingData.v
index a9a668ee..224decd5 100644
--- a/theories/Generic/DerivingData.v
+++ b/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,9 +46,9 @@ 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} 
@@ -56,19 +56,20 @@ Fixpoint dataMatch (T : Type) (X : T -> Type) (d : data X) {struct d}
     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).
+*)
\ No newline at end of file
diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
index a2afa91e..59b2cf1c 100644
--- a/theories/Programming/Show.v
+++ b/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.
 
diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
index daae245e..68775ee6 100644
--- a/theories/Structures/FunctorLaws.v
+++ b/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.
diff --git a/theories/Structures/Identity.v b/theories/Structures/Identity.v
index ab27fe44..95bad0ef 100644
--- a/theories/Structures/Identity.v
+++ b/theories/Structures/Identity.v
@@ -3,20 +3,24 @@ Require Import ExtLib.Core.Type.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Section ident.
-  Polymorphic Variable A : Type.
-  Context {tA : type A}.
-  Context {tokA : typeOk tA}.
+Polymorphic Class IsIdent@{t}
+            {A : Type@{t}}
+            {tA : type A}
+            {tokA : typeOk tA} (f : A -> A) : Prop :=
+  isId : forall x, proper x -> equal (f x) x.
 
-  Polymorphic Class IsIdent (f : A -> A) : Prop :=
-    isId : forall x, proper x -> equal (f x) x.
+Polymorphic Definition IsIdent_id@{t}
+            {A : Type@{t}}
+            {tA : type A}
+            {tokA : typeOk tA} : IsIdent id.
+Proof.
+  unfold id. eapply equiv_prefl; auto.
+Qed.
+Global Existing Instance IsIdent_id.
 
-  Global Polymorphic Instance IsIdent_id : IsIdent id.
-  Proof.
-    unfold id. eapply equiv_prefl; auto.
-  Qed.
-
-  Global Polymorphic Instance IsIdent_id' : IsIdent (fun x => x) := IsIdent_id.
-
-End ident.
 
+Polymorphic Definition IsIdent_id'@{t}
+            {A : Type@{t}}
+            {tA : type A}
+            {tokA : typeOk tA} : IsIdent (fun x => x) := IsIdent_id.
+Global Existing Instance IsIdent_id'.
diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
index 08170035..0b2ba79a 100644
--- a/theories/Structures/MonadLaws.v
+++ b/theories/Structures/MonadLaws.v
@@ -9,6 +9,7 @@ Require Import ExtLib.Data.Unit.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section MonadLaws.
   Variable m : Type@{d} -> Type.
   Variable M : Monad m.
@@ -168,3 +169,4 @@ Section MonadLaws.
   }.
 
 End MonadLaws.
+*)
\ No newline at end of file
diff --git a/theories/Structures/MonadWriter.v b/theories/Structures/MonadWriter.v
index 78ace55c..06116f6c 100644
--- a/theories/Structures/MonadWriter.v
+++ b/theories/Structures/MonadWriter.v
@@ -4,23 +4,27 @@ Require Import ExtLib.Structures.Monoid.
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.
 
-Polymorphic Class MonadWriter (T : Type@{s}) (M : Monoid T)
-            (m : Type@{d} -> Type) : Type :=
+Polymorphic Class MonadWriter@{d c s} (T : Type@{s}) (M : Monoid T)
+            (m : Type@{d} -> Type@{c}) : Type :=
 { tell : T -> m unit
 ; listen : forall {A : Type@{d}}, m A -> m (A * T)%type
 ; pass : forall {A : Type@{d}}, m (A * (T -> T))%type -> m A
 }.
 
-Section WriterOps.
-  Polymorphic Context {m : Type -> Type}.
-  Polymorphic Context {S : Type}.
-  Context {Monad_m : Monad m}.
-  Variable Monoid_S : Monoid S.
-  Context {Writer_m : MonadWriter Monoid_S m}.
+Polymorphic Definition listens@{d c s}
+            {m : Type@{d} -> Type@{c}}
+            {S : Type@{s}}
+            {Monad_m : Monad m}
+            {Monoid_S : Monoid S}
+            {Writer_m : MonadWriter Monoid_S m}
+            {A B : Type@{d}} (f : S -> B) (c : m A) : m (A * B)%type :=
+  liftM (fun x => (fst x, f (snd x))) (listen c).
 
-  Polymorphic Definition listens {A B : Type} (f : S -> B) (c : m A) : m (A * B) :=
-    liftM (fun x => (fst x, f (snd x))) (listen c).
-
-  Polymorphic Definition censor {A : Type} (f : S -> S) (c : m A) : m A :=
-    pass (liftM (fun x => (x, f)) c).
-End WriterOps.
+Polymorphic Definition censor@{d c s}
+            {m : Type@{d} -> Type@{c}}
+            {S : Type@{s}}
+            {Monad_m : Monad m}
+            {Monoid_S : Monoid S}
+            {Writer_m : MonadWriter Monoid_S m}
+            {A : Type@{d}} (f : S -> S) (c : m A) : m A :=
+  pass (liftM (fun x => (x, f)) c).
diff --git a/theories/Structures/Traversable.v b/theories/Structures/Traversable.v
index 739eca46..faae54ce 100644
--- a/theories/Structures/Traversable.v
+++ b/theories/Structures/Traversable.v
@@ -3,12 +3,20 @@ Require Import ExtLib.Structures.Applicative.
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 
-Polymorphic Class Traversable (T : Type@{d} -> Type@{r}) : Type :=
-{ mapT : forall {F : Type@{r} -> Type } {Ap:Applicative F} {A B : Type@{d}}, (A -> F B) -> T A -> F (T B) }.
+Polymorphic 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)
+}.
 
-Section traversable.
-
-  Polymorphic Definition sequence {T : Type@{d} -> Type@{d}} {Tr:Traversable T} {F : Type@{d} -> Type@{d}} {Ap:Applicative F} {A : Type@{d}}
+Polymorphic Definition sequence@{d r}
+            {T : Type@{d} -> Type@{d}}
+            {Tr:Traversable T}
+            {F : Type@{d} -> Type@{d}} {Ap:Applicative F} {A : Type@{d}}
   : T (F A) -> F (T A) := mapT (@id _).
-  Polymorphic Definition forT  {T : Type@{d} -> Type@{d}} {Tr:Traversable T} {F : Type@{d} -> Type@{d}} {Ap:Applicative F} {A B : Type@{d}} (aT:T A) (f:A -> F B) : F (T B) := mapT f aT.
-End traversable.
+
+Polymorphic Definition forT@{d r}
+            {T : Type@{d} -> Type@{d}}
+            {Tr:Traversable T} {F : Type@{d} -> Type@{d}} {Ap:Applicative F}
+            {A B : Type@{d}} (aT:T A) (f:A -> F B) : F (T B)
+:= mapT f aT.
diff --git a/theories/Tactics/MonadTac.v b/theories/Tactics/MonadTac.v
index 94946dff..4b5f93be 100644
--- a/theories/Tactics/MonadTac.v
+++ b/theories/Tactics/MonadTac.v
@@ -7,6 +7,7 @@ Require Import ExtLib.Tactics.TypeTac.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(*
 Section monad.
   Context {m : Type -> Type}.
   Variable meq : forall T {tT : type T}, type (m T).
@@ -33,3 +34,4 @@ Section monad.
     intros. eapply bind_proper; eauto. solve_equal.
   Qed.
 End monad.
+*)
\ No newline at end of file