diff options
Diffstat (limited to 'test-suite/bugs/opened/3045.v')
| -rw-r--r-- | test-suite/bugs/opened/3045.v | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v deleted file mode 100644 index b7f40b4a..00000000 --- a/test-suite/bugs/opened/3045.v +++ /dev/null @@ -1,30 +0,0 @@ -Set Asymmetric Patterns. -Generalizable All Variables. -Set Implicit Arguments. -Set Universe Polymorphism. - -Record SpecializedCategory (obj : Type) := - { - Object :> _ := obj; - Morphism : obj -> obj -> Type; - - Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' - }. - -Arguments Compose {obj} [C s d d'] m1 m2 : rename. - -Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := -| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. - -Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d := - match m in @ReifiedMorphism objC C s d return Morphism C s d with - | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1) - (@ReifiedMorphismDenote _ _ _ _ m2) - end. - -Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d) -: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }. -refine match m with - | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _ - end; clear m. -Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ]. |