diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-11 15:46:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-11 15:46:17 +0200 |
| commit | 1c620d266885086e076011917d5b1d28af299ea1 (patch) | |
| tree | 0c646e7b10a45a7c5e462270cb4a5d406e3cdf6b /test-suite/bugs/opened | |
| parent | 5f5198673cb8688e746861929e96160e04396ee9 (diff) | |
Move bug # 3368 to closed bugs
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3368.v | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test-suite/bugs/opened/3368.v b/test-suite/bugs/opened/3368.v deleted file mode 100644 index c0c00b4ed..000000000 --- a/test-suite/bugs/opened/3368.v +++ /dev/null @@ -1,15 +0,0 @@ -(* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *) -Set Universe Polymorphism. -Set Primitive Projections. -Record PreCategory := { object :> Type; morphism : object -> object -> Type }. -Record Functor (C D : PreCategory) := - { object_of :> C -> D; - morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. -Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory C (fun s d => morphism C d s). -Fail Definition opposite' C D (F : Functor C D) - := Build_Functor (opposite C) (opposite D) - (object_of F) - (fun s d => @morphism_of C D F s d). -(* Toplevel input, characters 15-191: -Anomaly: File "pretyping/reductionops.ml", line 149, characters 4-10: Assertion failed. -Please report. *) |