diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-06 15:24:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-06 15:24:36 +0100 |
| commit | 09193eeaf521c88e07a02d9088538f09561162ac (patch) | |
| tree | a985d706804a441cb66e6f7312160afb25c3f572 /test-suite/bugs/closed/2830.v | |
| parent | e6c2dc742732e0b2db83585b4099beb1f284143f (diff) | |
Fixing test for bug #2830.
Diffstat (limited to 'test-suite/bugs/closed/2830.v')
| -rw-r--r-- | test-suite/bugs/closed/2830.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index 8149065e7..219838aa3 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -122,7 +122,6 @@ Require Import Setoid. Module C. Reserved Notation "a ~> b" (at level 70, right associativity). -Reserved Notation "a ∘ b" (at level 45). Reserved Notation "a ≈ b" (at level 54). Generalizable All Variables. @@ -193,7 +192,7 @@ Definition skel {A:Type} : relation A := @eq A. Instance skel_equiv A : Equivalence (@skel A). Admitted. -Require Import FunctionalExtensionality. +Import FunctionalExtensionality. Instance set_cat : Category Type (fun A B => A -> B) := { id := fun A => fun x => x ; comp c b a f g := fun x => f (g x) @@ -205,7 +204,7 @@ intros. compute. reflexivity. Defined. (* The [list] type constructor is a Functor. *) -Require Import List. +Import List. Definition setList (A:set_cat) := list A. Instance list_functor : Functor set_cat set_cat setList. |