diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 13:46:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 13:46:56 +0200 |
| commit | 347c4888e07cf76c7e1c6672ccfa89f86a0f11ea (patch) | |
| tree | 083133886b1fa53fdcd064f6b98fa9f3a23004be /test-suite/bugs/closed/3648.v | |
| parent | 0307d06ac50caaa38d980a05f6ac3b0685720411 (diff) | |
Fix test-suite files which failed due to usage of $(admit)$ which
now fails with Error: Already an existential evar of name Main
Diffstat (limited to 'test-suite/bugs/closed/3648.v')
| -rw-r--r-- | test-suite/bugs/closed/3648.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v index 1256d125f..ba6006ed9 100644 --- a/test-suite/bugs/closed/3648.v +++ b/test-suite/bugs/closed/3648.v @@ -49,13 +49,11 @@ Record Functor (C D : PreCategory) := }. Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - +Axiom cheat : forall {A}, A. Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }. Definition functor_category (C D : PreCategory) : PreCategory. exact (@Build_PreCategory (Functor C D) - (@NaturalTransformation C D) - $(admit)$ - $(admit)$). + (@NaturalTransformation C D) cheat cheat). Defined. Local Notation "C -> D" := (functor_category C D) : category_scope. |