From ee71d144bd2a171532d9243198538c93aebb8a58 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 7 Jan 2020 18:26:24 -0500
Subject: [PATCH] Remove P*

---
 .gitignore                               |   3 +
 _CoqProject                              |   4 -
 examples/MonadReasoning.v                |   3 +-
 scratch/notation.md                      |  12 +-
 theories/Core/Type.v                     | 139 -----------------------
 theories/Data/Fun.v                      |   6 -
 theories/Data/HList.v                    |  50 --------
 theories/Data/List.v                     |  37 ------
 theories/Data/Map/FMapPositive.v         |  16 ---
 theories/Data/Member.v                   |   4 +-
 theories/Data/Monads/FuelMonadLaws.v     |   6 +-
 theories/Data/Monads/IdentityMonadLaws.v |   4 +-
 theories/Data/Monads/OptionMonadLaws.v   |   5 +-
 theories/Data/Monads/ReaderMonadLaws.v   |   5 +-
 theories/Data/N.v                        |  19 ----
 theories/Data/Nat.v                      |  20 +---
 theories/Data/Option.v                   |  37 ------
 theories/Data/PreFun.v                   |  65 -----------
 theories/Data/Prop.v                     |  14 +--
 theories/Data/Set/ListSet.v              |   8 +-
 theories/Data/SigT.v                     |  58 ----------
 theories/Data/Unit.v                     |  17 ---
 theories/Structures/Applicative.v        |   6 -
 theories/Structures/Foldable.v           |   3 +-
 theories/Structures/Functor.v            |  18 +--
 theories/Structures/FunctorLaws.v        |  18 +--
 theories/Structures/Identity.v           |  26 -----
 theories/Structures/Monad.v              |  39 +------
 theories/Structures/MonadLaws.v          |   4 +-
 theories/Structures/Monoid.v             |   9 +-
 theories/Structures/Proper.v             |  39 -------
 theories/Tactics/MonadTac.v              |   5 +-
 theories/Tactics/TypeTac.v               |  37 ------
 33 files changed, 34 insertions(+), 702 deletions(-)
 delete mode 100644 theories/Core/Type.v
 delete mode 100644 theories/Structures/Identity.v
 delete mode 100644 theories/Structures/Proper.v
 delete mode 100644 theories/Tactics/TypeTac.v

diff --git a/.gitignore b/.gitignore
index 000c79cd..9b37996c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,6 @@ deps.pdf
 .coqdeps.d
 .DS_Store
 html
+*.coq.d
+*.vok
+*.vos
diff --git a/_CoqProject b/_CoqProject
index a79cc488..187c2533 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,7 +7,6 @@ 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
@@ -18,7 +17,6 @@ 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
@@ -33,7 +31,6 @@ 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
@@ -104,7 +101,6 @@ 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
diff --git a/examples/MonadReasoning.v b/examples/MonadReasoning.v
index 94c2eece..6961b8e1 100644
--- a/examples/MonadReasoning.v
+++ b/examples/MonadReasoning.v
@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.PreFun.
@@ -57,4 +56,4 @@ Section with_m.
   Qed.
 
 End with_m.
-*)
\ No newline at end of file
+*)
diff --git a/scratch/notation.md b/scratch/notation.md
index f20b472d..7aaa3d3b 100644
--- a/scratch/notation.md
+++ b/scratch/notation.md
@@ -1,13 +1,13 @@
 Module | Notation | Definition | Level | Associativity
 ---|---|---|---|---
 `FunNotation` | `begin e1 end` | `e1` | 0 |
-`FunctorNotation` | `f <$> x` | `pfmap f x` | 52 | left
+`FunctorNotation` | `f <$> x` | `fmap f x` | 52 | left
 `ApplicativeNotation` | `f <*> x` | `ap f x` | 52 | left
 `MonadPlusNotation` | `x <+> y` | `mplus x y` | 54 | left
-`MonadNotation` | `f =<< c` | `pbind c f` | 61 | right
+`MonadNotation` | `f =<< c` | `bind c f` | 61 | right
 `MonadNotation` | `f >=> g` | `mcompose f g` | 61 | right
-`MonadNotation` | `x <- c1 ;; c2` | `pbind c1 (fun x => c2)` | 61 | right
-`MonadNotation` | `' pat <- c1 ;; c2` | `pbind c1 (fun x => match x with pat => c2)` | 61 | right
-`MonadNotation` | `c >>= f` | `pbind c f` | 62 | left
+`MonadNotation` | `x <- c1 ;; c2` | `bind c1 (fun x => c2)` | 61 | right
+`MonadNotation` | `' pat <- c1 ;; c2` | `bind c1 (fun x => match x with pat => c2)` | 61 | right
+`MonadNotation` | `c >>= f` | `bind c f` | 62 | left
 `MonadNotation` | `e1 ;; e2` | `_ <- e1 ;; e2` | 62 | left
-`FunNotation` | `f $ x` | `f x` | 99 | right
\ No newline at end of file
+`FunNotation` | `f $ x` | `f x` | 99 | right
diff --git a/theories/Core/Type.v b/theories/Core/Type.v
deleted file mode 100644
index 66f483e1..00000000
--- a/theories/Core/Type.v
+++ /dev/null
@@ -1,139 +0,0 @@
-Require Import Coq.Setoids.Setoid.
-Require Import ExtLib.Structures.Proper.
-
-Set Universe Polymorphism.
-
-(** Types are defined by their equivalence relations
- ** Proper elements are the elements for which the equivalence
- ** relation is reflexive.
- **)
-Class type@{t} (T : Type@{t}) : Type :=
-{ equal : T -> T -> Prop
-; proper : T -> Prop
-}.
-
-Definition type_from_equal@{t} {T : Type@{t}} (r : T -> T -> Prop) : type@{t} T :=
-{| equal := r
- ; proper := fun x => r x x
- |}.
-
-Definition type_libniz@{t} (T : Type@{t}) : type@{t} T :=
-{| equal := @eq T
- ; proper := fun _ => True
- |}.
-
-Existing Class proper.
-
-Section type.
-  Universe u.
-  Context {T : Type@{u}}.
-  Variable tT : type T.
-(*
-  Global Instance Proper_type : Proper T :=
-  { proper := fun x => equal x x }.
-*)
-  Class typeOk@{} :=
-  { only_proper : forall x y, equal x y -> proper x /\ proper y
-  ; equiv_prefl :> PReflexive proper equal
-  ; equiv_sym :> Symmetric equal
-  ; equiv_trans :> Transitive equal
-  }.
-
-  Global Instance proper_left@{} :
-    typeOk ->
-    forall x y : T, equal x y -> proper x.
-  Proof.
-    clear. intros.
-    match goal with
-    | H : equal _ _ |- _ => eapply only_proper in H
-    end; intuition.
-  Qed.
-  Global Instance proper_right@{} :
-    typeOk ->
-    forall x y : T, equal x y -> proper y.
-  Proof.
-    clear. intros.
-    match goal with
-    | H : equal _ _ |- _ => eapply only_proper in H
-    end; intuition.
-  Qed.
-
-End type.
-
-
-Definition type1@{d r z} (F : Type@{d} -> Type@{r}) : Type@{z} :=
-  forall {T:Type@{d}}, type@{d} T -> type@{r} (F T).
-
-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).
-
-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).
-
-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).
-
-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).
-
-Definition typeOk3@{t u v w z} F (tF : type3 F) : Type@{z} :=
-  forall (T : Type@{t}) (tT : type T), @typeOk@{t} T tT -> typeOk2@{u v w z} _ (tF _ tT).
-
-Existing Class type1.
-Existing Class type2.
-Existing Class type3.
-
-Global Instance type_type1 F (tF : type1 F) T (tT : type T) : type (F T) :=
-  tF _ tT.
-
-Global Instance type1_type2 F (tF : type2 F) T (tT : type T) : type1 (F T) :=
-  tF _ tT.
-
-Global Instance type2_type3 F (tF : type3 F) T (tT : type T) : type2 (F T) :=
-  tF _ tT.
-
-Class Oktype T : Type :=
-{ the_type :> type T
-; the_proof :> typeOk the_type
-}.
-
-Coercion the_type : Oktype >-> type.
-
-Global Instance typeOk_typeOk1 F (tF : type1 F) T (tT : type T) : type (F T) :=
-  tF _ tT.
-
-Global Instance typeOk1_typeOk2 F (tF : type2 F) T (tT : type T) : type1 (F T) :=
-  tF _ tT.
-
-Global Instance typeOk2_typeOk3 F (tF : type3 F) T (tT : type T) : type2 (F T) :=
-  tF _ tT.
-
-
-Section typeOk_from_equal.
-  Universe u.
-  Context {T : Type@{u}} (r : relation T).
-  Hypothesis p : forall x y, r x y -> r x x /\ r y y.
-  Hypothesis sym : Symmetric r.
-  Hypothesis trans : Transitive r.
-
-  Theorem typeOk_from_equal@{} : typeOk (type_from_equal r).
-  Proof.
-    constructor; auto.
-    { simpl. red. auto. }
-  Qed.
-End typeOk_from_equal.
-
-Theorem typeOk_libniz@{u} (T : Type@{u}) : typeOk (type_libniz T).
-Proof.
-  constructor; unfold equal, type_libniz; auto with typeclass_instances.
-  { split; exact I. }
-Qed.
-
-(*
-Add Parametric  Relation (T : Type) (tT : type T) (tokT : typeOk tT) : T (@equal _ tT)
-  symmetry proved by (@equiv_sym _ _ _)
-  transitivity proved by (@equiv_trans _ _ _)
-  as equal_rel.
-*)
diff --git a/theories/Data/Fun.v b/theories/Data/Fun.v
index 479853a1..0f9fb14f 100644
--- a/theories/Data/Fun.v
+++ b/theories/Data/Fun.v
@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.PreFun.
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
@@ -8,11 +7,6 @@ Require Import ExtLib.Structures.Monoid.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Global Instance proper_id (T : Type) {tT : type T} : proper (fun x => x).
-Proof.
-  repeat red; intros. apply H.
-Qed.
-
 
 Section functors.
   Variable A : Type.
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index 03b63075..7039ef92 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -1,8 +1,6 @@
 Require Import Coq.Lists.List.
 Require Import Relations RelationClasses.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Data.SigT.
 Require Import ExtLib.Data.Member.
 Require Import ExtLib.Data.ListNth.
@@ -453,54 +451,6 @@ Section hlist.
   Qed.
 
   Section type.
-    Variable eqv : forall x, type (F x).
-
-    Global Instance type_hlist (ls : list iT): type (hlist ls) :=
-    { equal := @equiv_hlist (fun x => @equal _ (eqv x)) ls
-    ; proper :=
-      (fix recur ls (h : hlist ls) : Prop :=
-        match h with
-          | Hnil => True
-          | Hcons _ _ x y => proper x /\ recur _ y
-        end) ls
-    }.
-
-    Variable eqvOk : forall x, typeOk (eqv x).
-
-    Global Instance typeOk_hlist (ls : list iT): typeOk (type_hlist ls).
-    Proof.
-      constructor.
-      { induction ls; intros.
-        { rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
-          clear. compute; auto. }
-        { rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
-          simpl in H.
-          inv_all. eapply IHls in H1.
-          eapply only_proper in H0; eauto.
-          simpl; tauto. } }
-      { intro. induction ls; simpl.
-        { rewrite (hlist_eta x); intros; constructor. }
-        { rewrite (hlist_eta x); intros; intuition; constructor.
-          eapply preflexive; [ | eauto with typeclass_instances ].
-          eauto with typeclass_instances.
-          eapply IHls; eauto. } }
-      { red. induction 1.
-        { constructor. }
-        { constructor. symmetry. assumption. assumption. } }
-      { red. induction 1.
-        { auto. }
-        { intro H1.
-          etransitivity; [ | eassumption ].
-          constructor; eauto. } }
-    Qed.
-
-    Global Instance proper_hlist_app l l' : proper (@hlist_app l l').
-    Proof.
-      do 6 red. induction 1; simpl; auto.
-      { intros. constructor; eauto.
-        eapply IHequiv_hlist. exact H1. }
-    Qed.
-
     Lemma hlist_app_assoc : forall ls ls' ls''
                                  (a : hlist ls) (b : hlist ls') (c : hlist ls''),
       hlist_app (hlist_app a b) c =
diff --git a/theories/Data/List.v b/theories/Data/List.v
index e5b401b3..03e4fabe 100644
--- a/theories/Data/List.v
+++ b/theories/Data/List.v
@@ -1,6 +1,5 @@
 Require Import Coq.Lists.List.
 Require Coq.Classes.EquivDec.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
@@ -12,42 +11,6 @@ Set Implicit Arguments.
 Set Strict Implicit.
 Set Universe Polymorphism.
 
-Section type.
-  Universe u.
-  Variable T : Type@{u}.
-  Context {type_T : type T}.
-
-  Inductive list_eq@{} : list T -> list T -> Prop :=
-  | nil_eq : list_eq nil nil
-  | cons_eq : forall x xs y ys, equal x y -> list_eq xs ys -> list_eq (x :: xs) (y :: ys).
-
-  Instance type_list@{} : type@{u} (list T) :=
-  { equal := list_eq
-  ; proper := Forall proper
-  }.
-
-  Context {typeOk_T : typeOk type_T}.
-
-  Instance typeOk_list@{} : typeOk type_list.
-  Proof.
-    constructor.
-    { intros. induction H.
-      { intuition; constructor. }
-      { apply only_proper in H; auto. intuition; constructor; intuition. } }
-    { intro. induction x; intros.
-      { constructor. }
-      { inversion H; clear H; subst.
-        constructor; auto.
-        apply equiv_prefl; auto. apply IHx. apply H3. } }
-    { intro. induction 1; constructor; auto.
-      apply equiv_sym; auto. }
-    { intro. do 3 intro.  revert z. induction H.
-      { remember nil. destruct 1; try congruence. constructor. }
-      { remember (y :: ys). destruct 1; try congruence. inversion Heql; clear Heql; subst.
-        constructor. eapply equiv_trans; eauto. eapply IHlist_eq. apply H2. } }
-  Qed.
-End type.
-
 Section EqDec.
   Universe u.
   Variable T : Type@{u}.
diff --git a/theories/Data/Map/FMapPositive.v b/theories/Data/Map/FMapPositive.v
index 9fc94edb..878e4b6e 100644
--- a/theories/Data/Map/FMapPositive.v
+++ b/theories/Data/Map/FMapPositive.v
@@ -282,21 +282,5 @@ Section fmap.
 
 End fmap.
 
-Require Import ExtLib.Core.Type.
-
-Section type.
-  Variable T : Type.
-  Variable tT : type T.
-
-  Instance type_pmap : type (pmap T) :=
-    type_from_equal
-      (fun l r =>
-            (forall k v,
-               mapsto k v l -> exists v', mapsto k v' r /\ equal v v')
-         /\ (forall k v,
-               mapsto k v r -> exists v', mapsto k v' l /\ equal v v')).
-
-End type.
-
 Global Instance Functor_pmap : Functor pmap :=
 { fmap := fmap_pmap }.
diff --git a/theories/Data/Member.v b/theories/Data/Member.v
index 105fba7a..6a806c35 100644
--- a/theories/Data/Member.v
+++ b/theories/Data/Member.v
@@ -1,12 +1,10 @@
 (** [member] is the proof relevant version of [In] **)
 Require Import Coq.Lists.List.
 Require Import Relations RelationClasses.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.SigT.
 Require Import ExtLib.Data.ListNth.
 Require Import ExtLib.Data.Option.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Tactics.Injection.
 Require Import ExtLib.Tactics.EqDep.
 
@@ -137,4 +135,4 @@ Section member.
     induction 1; simpl; auto.
   Qed.
 
-End member.
\ No newline at end of file
+End member.
diff --git a/theories/Data/Monads/FuelMonadLaws.v b/theories/Data/Monads/FuelMonadLaws.v
index df6989e9..225f6fba 100644
--- a/theories/Data/Monads/FuelMonadLaws.v
+++ b/theories/Data/Monads/FuelMonadLaws.v
@@ -1,14 +1,10 @@
 Require Import RelationClasses.
 Require Import Setoid.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.MonadLaws.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Data.Monads.FuelMonad.
-Require Import ExtLib.Data.N.
-Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -146,4 +142,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 1280cd08..7e028620 100644
--- a/theories/Data/Monads/IdentityMonadLaws.v
+++ b/theories/Data/Monads/IdentityMonadLaws.v
@@ -1,10 +1,8 @@
 Require Import Coq.Classes.RelationClasses.
 Require Import Setoid.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.MonadLaws.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Data.Monads.IdentityMonad.
 
 Set Implicit Arguments.
@@ -63,4 +61,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 7084b7ad..a1f57f29 100644
--- a/theories/Data/Monads/OptionMonadLaws.v
+++ b/theories/Data/Monads/OptionMonadLaws.v
@@ -1,13 +1,10 @@
 Require Import RelationClasses.
 Require Import Setoid.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Monads.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.Option.
 Require Import ExtLib.Data.Monads.OptionMonad.
-Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -295,4 +292,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 8fc126cd..9b3abe81 100644
--- a/theories/Data/Monads/ReaderMonadLaws.v
+++ b/theories/Data/Monads/ReaderMonadLaws.v
@@ -1,12 +1,9 @@
 Require Import RelationClasses.
 Require Import Setoid.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Monads.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.Monads.ReaderMonad.
-Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -94,4 +91,4 @@ Section Laws.
 *)
 
 End Laws.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Data/N.v b/theories/Data/N.v
index 94a948e5..b15e7289 100644
--- a/theories/Data/N.v
+++ b/theories/Data/N.v
@@ -1,20 +1 @@
 Require Import BinPos.
-Require Import ExtLib.Core.Type.
-Require Import ExtLib.Structures.Proper.
-
-Global Instance type_N : type N :=
-{ equal := @eq N 
-; proper := fun _ => True
-}.
-
-Global Instance typeOk_N : typeOk type_N.
-Proof.
-  constructor.
-  { compute; auto. }
-  { compute; auto. }
-  { compute; auto. }
-  { compute. intros. etransitivity; eauto. }
-Qed.
-
-Global Instance N_proper (n : N) : proper n.
-Proof. exact I. Qed.
\ No newline at end of file
diff --git a/theories/Data/Nat.v b/theories/Data/Nat.v
index 88ef9f06..49e0beba 100644
--- a/theories/Data/Nat.v
+++ b/theories/Data/Nat.v
@@ -1,6 +1,5 @@
 Require Coq.Arith.Arith.
 Require Import ExtLib.Core.RelDec.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Tactics.Injection.
@@ -12,23 +11,6 @@ Set Strict Implicit.
 Global Instance RelDec_eq : RelDec (@eq nat) :=
 { rel_dec := EqNat.beq_nat }.
 
-Global Instance type_nat : type nat :=
-{ equal := @eq nat
-; proper := fun _ => True
-}.
-
-Global Instance typeOk_nat : typeOk type_nat.
-Proof.
-  constructor.
-  { compute; auto. }
-  { compute; auto. }
-  { compute; auto. }
-  { compute. intros. etransitivity; eauto. }
-Qed.
-
-Global Instance nat_proper (n : nat) : proper n.
-Proof. exact I. Qed.
-
 Require Coq.Numbers.Natural.Peano.NPeano.
 
 Global Instance RelDec_lt : RelDec lt :=
@@ -110,4 +92,4 @@ Definition nat_get_eq (n m : nat) (pf : unit -> n = m) : n = m :=
   match PeanoNat.Nat.eq_dec n m with
   | left pf => pf
   | right bad => match bad (pf tt) with end
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/Data/Option.v b/theories/Data/Option.v
index addfd4a9..153c9b17 100644
--- a/theories/Data/Option.v
+++ b/theories/Data/Option.v
@@ -1,14 +1,12 @@
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Classes.Morphisms.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Structures.Traversable.
 Require Import ExtLib.Structures.Applicative.
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.FunctorLaws.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Tactics.Injection.
 Require Import ExtLib.Tactics.Consider.
@@ -101,41 +99,6 @@ Section relation.
 
 End relation.
 
-Section type.
-  Variable T : Type.
-  Variable tT : type T.
-
-  Global Instance type_option : type (option T) :=
-  { equal := Roption equal
-  ; proper := fun x => match x with
-                         | None => True
-                         | Some y => proper y
-                       end }.
-
-  Variable tTOk : typeOk tT.
-
-  Global Instance typeOk_option : typeOk type_option.
-  Proof.
-    constructor.
-    { inversion 1.
-      split; constructor.
-      split; simpl; eapply only_proper; eauto. symmetry; eauto. }
-    { red. destruct x; simpl. constructor.
-      eapply preflexive; [ | eapply H ].
-      eapply equiv_prefl; auto. constructor. }
-    { red. destruct 1. constructor. constructor. symmetry. assumption. }
-    { red. destruct 1; inversion 1; subst. assumption.
-      constructor. etransitivity; eauto. }
-  Qed.
-
-  Global Instance proper_Some : proper (@Some T).
-  Proof. constructor; assumption. Qed.
-
-  Global Instance proper_None : proper (@None T).
-  Proof. constructor. Qed.
-
-End type.
-
 (*
 Global Instance FunctorLaws_option : FunctorLaws Functor_option type_option.
 Proof.
diff --git a/theories/Data/PreFun.v b/theories/Data/PreFun.v
index 3a3bd788..af9cf398 100644
--- a/theories/Data/PreFun.v
+++ b/theories/Data/PreFun.v
@@ -1,7 +1,5 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relations.
-Require Import ExtLib.Structures.Proper.
-Require Import ExtLib.Core.Type.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -9,69 +7,6 @@ Set Universe Polymorphism.
 
 Definition Fun@{d c} (A : Type@{d}) (B : Type@{c}) := A -> B.
 
-Section type.
-  Universe uT uU.
-  Variables (T : Type@{uT}) (U : Type@{uU}) (tT : type T) (tU : type U).
-
-  Global Instance type_Fun@{uU'} : type@{uU'} (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).
-
-  Global Instance typeOk_Fun@{uU'} : typeOk@{uU'} type_Fun.
-  Proof.
-    constructor.
-    { unfold equiv. simpl. unfold respectful.
-      destruct tOk. destruct uOk; intros.
-      split; intros.
-      { destruct (only_proper _ _ H0).
-        etransitivity. eapply H. eassumption.
-        symmetry. eapply H. symmetry. auto. }
-      { destruct (only_proper _ _ H0).
-        symmetry. etransitivity; [ | eapply H ].
-        symmetry. eapply H. eassumption. symmetry. eauto. } }
-    { red. intros. apply H. }
-    { compute. intuition. symmetry. eapply H. symmetry. auto. }
-    { simpl; intro; intros. intuition. red in H; red in H0; simpl in *.
-      red; intros.
-      etransitivity. eapply H. eassumption.
-      eapply H0.
-      eapply only_proper in H1; intuition.
-      eapply preflexive with (wf := proper); auto.
-      apply tOk. }
-  Qed.
-
-  Global Instance proper_app@{uU'} : forall (f : T -> U) (a : T),
-    proper@{uU'} f -> proper a -> proper (f a).
-  Proof.
-    simpl; intros. red in H.
-    eapply proper_left; eauto.
-    eapply H. eapply preflexive. eapply equiv_prefl; auto. auto.
-  Qed.
-
-  Theorem proper_fun@{uU'} : forall (f : T -> U),
-    (forall x y, equal x y -> equal (f x) (f y)) ->
-    proper@{uU'} f.
-  Proof.
-    intros. do 3 red. eauto.
-  Qed.
-
-  Theorem equal_fun@{uU'} : forall (f g : T -> U),
-    (forall x y, equal x y -> equal (f x) (g y)) ->
-    equal@{uU'} f g.
-  Proof. intros. do 3 red. apply H. Qed.
-
-  Theorem equal_app@{uU'} : forall (f g : T -> U) (x y : T),
-    equal@{uU'} f g -> equal x y ->
-    equal (f x) (g y).
-  Proof.
-    clear. intros. do 3 red in H. auto.
-  Qed.
-
-End type.
-
 Definition compose@{uA uB uC} {A:Type@{uA}} {B:Type@{uB}} {C : Type@{uC}}
     (g : B -> C) (f : A -> B) : A -> C :=
   fun x => g (f x).
diff --git a/theories/Data/Prop.v b/theories/Data/Prop.v
index 1bf0093e..60255252 100644
--- a/theories/Data/Prop.v
+++ b/theories/Data/Prop.v
@@ -1,14 +1,4 @@
-Require Import ExtLib.Core.Type.
-
-Global Instance type_Prop : type Prop :=
-{ equal := iff
-; proper := fun _ => True
-}.
-
-Global Instance typeOk_Prop : typeOk type_Prop.
-Proof.
-  constructor; compute; firstorder.
-Qed.
+From Coq Require Import Setoid.
 
 (** NOTE: These should fit into a larger picture, e.g. lattices or monoids **)
 (** And/Conjunction **)
@@ -110,4 +100,4 @@ Proof.
 Qed.
 
 Lemma iff_eq : forall (P Q : Prop), P = Q -> (P <-> Q).
-Proof. clear. intros; subst; reflexivity. Qed.
\ No newline at end of file
+Proof. clear. intros; subst; reflexivity. Qed.
diff --git a/theories/Data/Set/ListSet.v b/theories/Data/Set/ListSet.v
index 437c7bb3..6abe029b 100644
--- a/theories/Data/Set/ListSet.v
+++ b/theories/Data/Set/ListSet.v
@@ -63,10 +63,6 @@ Global Instance Foldable_listset {T} (R : T -> T -> Prop)
   fun _ f a t => List.fold_left (fun x y => f y x) t a.
 
 Require Import ExtLib.Structures.Functor.
-Require Import ExtLib.Programming.Eqv.
 
-Global Instance PFunctor_listset : PFunctor lset :=
-{ FunP := fun t => { eqT : Eqv t & RelDec eqv }
-; pfmap := fun _ B eqv_dec f s => 
-  List.fold_left (fun acc x => lset_add (@rel_dec B (@eqv B (projT1 eqv_dec)) (projT2 eqv_dec)) (f x) acc) s (@lset_empty _)
-}.
+Global Instance Functor_listset : Functor lset :=
+{ fmap := map }.
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index 5934a72c..f452367f 100644
--- a/theories/Data/SigT.v
+++ b/theories/Data/SigT.v
@@ -1,70 +1,12 @@
 Require Coq.Classes.EquivDec.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.EqDep.
 Require Import ExtLib.Tactics.Injection.
 Require Import ExtLib.Tactics.EqDep.
-Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Printing Universes.
 
-Section type.
-  Variable T : Type.
-  Variable F : T -> Type.
-  Variable ED : EquivDec.EqDec _ (@eq T).
-  Variable tT : type T.
-  Variable typF : forall x, type (F x).
-
-  Global Instance type_sigT : type (sigT F) :=
-  { equal := fun x y =>
-    equal (projT1 x) (projT1 y) /\
-    exists pf : projT1 y = projT1 x,
-      equal (projT2 x) (match pf in _ = t return F t with
-                          | eq_refl => projT2 y
-                        end)
-  ; proper := fun x => proper (projT1 x) /\ proper (projT2 x)
-  }.
-
-  Variable typeOkT : typeOk tT.
-  Variable typOkF : forall x, typeOk (typF x).
-
-  Global Instance typeOk_sigT : typeOk type_sigT.
-  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. }
-    { red. destruct x; intros. do 2 red in H.
-      do 2 red; simpl in *. intuition.
-      try solve [ apply equiv_prefl; eauto ].
-      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.
-      etransitivity; eauto.
-      destruct H2; destruct H3; subst. exists eq_refl. etransitivity; eauto. }
-  Qed.
-
-  Global Instance proper_existT a b : proper a -> proper b -> proper (existT F a b).
-  Proof.
-    red; simpl. intuition.
-  Qed.
-
-  Global Instance proper_projT1 a : proper a -> proper (projT1 a).
-  Proof.
-    red; simpl. intuition.
-  Qed.
-
-  Global Instance proper_projT2 a : proper a -> proper (projT2 a).
-  Proof.
-    red; simpl. intuition.
-  Qed.
-
-End type.
-
 Section injective.
   Variable T : Type.
   Variable F : T -> Type.
diff --git a/theories/Data/Unit.v b/theories/Data/Unit.v
index 342fa510..eb36983e 100644
--- a/theories/Data/Unit.v
+++ b/theories/Data/Unit.v
@@ -1,6 +1,4 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
-Require Import ExtLib.Structures.Proper.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -10,18 +8,3 @@ Global Instance RelDec_eq_unit : RelDec (@eq unit) :=
 Global Instance RelDec_Correct_eq_unit : RelDec_Correct RelDec_eq_unit.
   constructor. destruct x; destruct y; auto; simpl. intuition.
 Qed.
-
-Global Instance type_unit : type unit :=
-{ equal := fun _ _ => True 
-; proper := fun _ => True
-}.
-
-Global Instance typeOk_N : typeOk type_unit.
-Proof.
-  constructor; compute; auto.
-Qed.
-
-Global Instance proper_tt (x : unit) : proper x.
-Proof.
-  exact I.
-Qed.
\ No newline at end of file
diff --git a/theories/Structures/Applicative.v b/theories/Structures/Applicative.v
index 65d3d5a6..a395b2b4 100644
--- a/theories/Structures/Applicative.v
+++ b/theories/Structures/Applicative.v
@@ -5,12 +5,6 @@ Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 Set Universe Polymorphism.
 
-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
-}.
-
 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
diff --git a/theories/Structures/Foldable.v b/theories/Structures/Foldable.v
index d567fbd2..b8423ad5 100644
--- a/theories/Structures/Foldable.v
+++ b/theories/Structures/Foldable.v
@@ -1,5 +1,4 @@
 Require Import Coq.Lists.List.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monoid.
 
 Set Implicit Arguments.
@@ -26,7 +25,7 @@ Section foldable.
   Variable Add : A -> T -> T -> Prop.
 
   Class FoldableOk : Type :=
-  { fold_ind : forall m (M : Monoid m) (t : type m) (ML : MonoidLaws M) (P : m -> Prop) f u,
+  { fold_ind : forall m (M : Monoid m) (ML : MonoidLaws M) (P : m -> Prop) f u,
                  P (monoid_unit M) ->
                  (forall x y z,
                     Add x y z ->
diff --git a/theories/Structures/Functor.v b/theories/Structures/Functor.v
index 24d2fe3d..2c1096ad 100644
--- a/theories/Structures/Functor.v
+++ b/theories/Structures/Functor.v
@@ -9,22 +9,6 @@ Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
 Polymorphic Definition ID@{d} {T : Type@{d}} (f : T -> T) : Prop :=
   forall x : T, f x = x.
 
-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.
-
-(** 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 52, left associativity).
+  Notation "f <$> x" := (@fmap _ _ _ _ f x) (at level 52, left associativity).
 End FunctorNotation.
diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
index 16a870f4..f3942087 100644
--- a/theories/Structures/FunctorLaws.v
+++ b/theories/Structures/FunctorLaws.v
@@ -1,8 +1,5 @@
 Require Import Coq.Relations.Relations.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.Fun.
-Require Import ExtLib.Structures.Identity.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Structures.Functor.
 
 Set Implicit Arguments.
@@ -14,20 +11,11 @@ Section laws.
   Class FunctorLaws@{t u X}
               (F : Type@{t} -> Type@{u})
               (Functor_F : Functor F)
-              (Feq : type1@{t u X} F)
   : Type :=
-  { 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_id : forall T (x : F T), fmap id x = x
   ; 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 ->
+                     (x : F T),
       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 : Type@{t}) (U : Type@{u}) (tT : type T) (tU : type U),
-      typeOk@{t} tT -> typeOk@{u} tU ->
-      proper (@fmap _ _ T U)
+        fmap (compose g f) x = fmap g (fmap f x)
   }.
 End laws.
diff --git a/theories/Structures/Identity.v b/theories/Structures/Identity.v
deleted file mode 100644
index 95bad0ef..00000000
--- a/theories/Structures/Identity.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Require Import ExtLib.Core.Type.
-
-Set Implicit Arguments.
-Set Strict Implicit.
-
-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 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.
-
-
-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/Monad.v b/theories/Structures/Monad.v
index 65c53fbb..e6950ea9 100644
--- a/theories/Structures/Monad.v
+++ b/theories/Structures/Monad.v
@@ -11,21 +11,6 @@ Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
 }.
 
-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
-}.
-
-Existing Class MonP.
-Hint Extern 0 (@MonP _ _ _) => progress (simpl MonP) : typeclass_instances.
-
-Global Instance PMonad_Monad@{d c p} (m : Type@{d} -> Type@{c}) (M : Monad m) : PMonad@{d c p} m :=
-{ MonP := Any
-; pret := fun _ _ x => ret x
-; pbind := fun _ _ _ c f => bind c f
-}.
-
 Section monadic.
 
   Definition liftM@{d c}
@@ -68,18 +53,18 @@ Module MonadNotation.
 
   Delimit Scope monad_scope with monad.
 
-  Notation "c >>= f" := (@pbind _ _ _ _ _ c f) (at level 62, left associativity) : monad_scope.
-  Notation "f =<< c" := (@pbind _ _ _ _ _ c f) (at level 61, right associativity) : monad_scope.
+  Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 62, left associativity) : monad_scope.
+  Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 61, right associativity) : monad_scope.
   Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope.
 
-  Notation "x <- c1 ;; c2" := (@pbind _ _ _ _ _ c1 (fun x => c2))
+  Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2))
     (at level 61, c1 at next level, right associativity) : monad_scope.
 
   Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
     (at level 62, left associativity) : monad_scope.
 
   Notation "' pat <- c1 ;; c2" :=
-    (@pbind _ _ _ _ _ c1 (fun x => match x with pat => c2 end))
+    (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))
     (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.
 
 End MonadNotation.
@@ -97,20 +82,4 @@ Global Instance Applicative_Monad@{} : Applicative m :=
 ; ap := @apM _ _
 }.
 
-Universe p.
-Context {PM : PMonad@{d c p} m}.
-
-Global Instance PFunctor_PMonad@{} : PFunctor m :=
-{ FunP := MonP
-; pfmap := fun _ _ _ f a =>
-  pbind a (fun x => pret (f x))
-}.
-
-Global Instance PApplicative_PMonad@{} : PApplicative m :=
-{ AppP := MonP
-; ppure := fun _ _ x => pret x
-; pap := fun _ _ _ f x =>
-  pbind f (fun f => pbind x (fun x => pret (f x)))
-}.
-
 End Instances.
diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
index 0b2ba79a..aa394dd6 100644
--- a/theories/Structures/MonadLaws.v
+++ b/theories/Structures/MonadLaws.v
@@ -1,8 +1,6 @@
 Require Import Setoid.
 Require Import Coq.Classes.Morphisms.
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monads.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Data.Unit.
 
@@ -169,4 +167,4 @@ Section MonadLaws.
   }.
 
 End MonadLaws.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Structures/Monoid.v b/theories/Structures/Monoid.v
index c6036eb9..ad73f08b 100644
--- a/theories/Structures/Monoid.v
+++ b/theories/Structures/Monoid.v
@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.BinOps.
 
 Set Implicit Arguments.
@@ -14,12 +13,10 @@ Section Monoid.
   ; monoid_unit : S
   }.
 
-  Context {Type_S : type S}.
-
   Class MonoidLaws@{} (M : Monoid) : Type :=
-  { monoid_assoc :> Associative M.(monoid_plus) equal
-  ; monoid_lunit :> LeftUnit M.(monoid_plus) M.(monoid_unit) equal
-  ; monoid_runit :> RightUnit M.(monoid_plus) M.(monoid_unit) equal
+  { monoid_assoc :> Associative M.(monoid_plus) eq
+  ; monoid_lunit :> LeftUnit M.(monoid_plus) M.(monoid_unit) eq
+  ; monoid_runit :> RightUnit M.(monoid_plus) M.(monoid_unit) eq
   }.
 
 End Monoid.
diff --git a/theories/Structures/Proper.v b/theories/Structures/Proper.v
deleted file mode 100644
index dc954ca9..00000000
--- a/theories/Structures/Proper.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Coq.Setoids.Setoid.
-Require Import Coq.Relations.Relations.
-Require Import Coq.Classes.RelationClasses.
-
-Set Implicit Arguments.
-Set Strict Implicit.
-
-(*
-Class Proper (T : Type) : Type :=
-  proper : T -> Prop.
-*)
-
-Section relations.
-  Context {T : Type} (wf : T -> Prop) (R : relation T).
-
-  Class PReflexive : Prop :=
-    preflexive : forall x : T, wf x -> R x x.
-
-  Global Instance PReflexive_Reflexive (r : Reflexive R) : PReflexive.
-  Proof. red; intros; reflexivity. Qed.
-
-  Class PSymmetric : Prop :=
-    psymmetric : forall x y, wf x -> wf y -> R x y -> R y x.
-
-  Global Instance PSymmetric_Symmetric (r : Symmetric R) : PSymmetric.
-  Proof. red; intros; symmetry; auto. Qed.
-
-  Class PTransitive : Prop :=
-    ptransitive : forall x y z, wf x -> wf y -> wf z ->
-      R x y -> R y z -> R x z.
-
-  Global Instance PTransitive_Transitive (r : Transitive R) : PTransitive.
-  Proof. intro; intros; etransitivity; eauto. Qed.
-
-End relations.
-
-Arguments PReflexive {T} wf R.
-Arguments PSymmetric {T} wf R.
-Arguments PTransitive {T} wf R.
diff --git a/theories/Tactics/MonadTac.v b/theories/Tactics/MonadTac.v
index 4b5f93be..ff090cd6 100644
--- a/theories/Tactics/MonadTac.v
+++ b/theories/Tactics/MonadTac.v
@@ -1,8 +1,5 @@
-Require Import ExtLib.Core.Type.
-Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.MonadLaws.
-Require Import ExtLib.Tactics.TypeTac.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -34,4 +31,4 @@ Section monad.
     intros. eapply bind_proper; eauto. solve_equal.
   Qed.
 End monad.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Tactics/TypeTac.v b/theories/Tactics/TypeTac.v
deleted file mode 100644
index ed843467..00000000
--- a/theories/Tactics/TypeTac.v
+++ /dev/null
@@ -1,37 +0,0 @@
-Require Import ExtLib.Core.Type.
-Require Import ExtLib.Data.Fun.
-Require Import ExtLib.Structures.Proper.
-
-Set Implicit Arguments.
-Set Strict Implicit.
-
-Hint Extern 1 (proper (fun x => _)) => apply proper_fun; intros : typeclass_instances.
-Hint Extern 1 (equal (fun x => _) _) => apply proper_fun; intros : typeclass_instances.
-Hint Extern 1 (equal _ (fun x => _)) => apply proper_fun; intros : typeclass_instances.
-Hint Extern 0 (PReflexive _) => eapply equiv_prefl.
-
-Ltac solve_proper :=
-  repeat match goal with 
-           | |- _ => solve [ eauto ]
-           | |- proper (fun x => _) => eapply proper_fun; intros; solve_equal
-           | |- _ => eapply proper_app; 
-             [ solve [ eauto with typeclass_instances ] 
-             | solve [ eauto with typeclass_instances ]
-             | solve_proper | solve_proper ]
-         end;
-  eauto with typeclass_instances
-with solve_equal :=
-  repeat match goal with
-           | |- _ => solve [ eauto ]
-           | |- equal ?X ?X => 
-             solve [ eapply preflexive with (wf := proper); eauto 100 with typeclass_instances ]
-           | |- equal (fun x => _) _ => eapply equal_fun; intros
-           | |- equal _ (fun x => _) => eapply equal_fun; intros
-           | |- _ => eapply equal_app
-         end; eauto with typeclass_instances.
-
-Ltac type_tac :=
-  match goal with
-    | |- proper _ => solve_proper
-    | |- equal _ _ => solve_equal
-  end.
\ No newline at end of file