diff options
author | 2014-09-26 13:30:19 +0200 | |
---|---|---|
committer | 2014-09-26 13:30:19 +0200 | |
commit | 9b1b8aba9cd40cc91fd9d52af4e6c075311ba4db (patch) | |
tree | 200b94e827381cda5102b518291eb1962adb8311 /test-suite/bugs/opened/3045.v | |
parent | 158398435d1727e59f933f3eff6b58c5a635ffb8 (diff) |
Add a bunch of reproduction files for bugs.
Diffstat (limited to 'test-suite/bugs/opened/3045.v')
-rw-r--r-- | test-suite/bugs/opened/3045.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v new file mode 100644 index 000000000..b7f40b4ad --- /dev/null +++ b/test-suite/bugs/opened/3045.v @@ -0,0 +1,30 @@ +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 [ [] ? ]. |