From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/opened/3045.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test-suite/bugs/opened/3045.v (limited to 'test-suite/bugs/opened/3045.v') diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v new file mode 100644 index 00000000..b7f40b4a --- /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 [ [] ? ]. -- cgit v1.2.3