Imported Upstream version 8.5~beta1+dfsg

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 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 [ [] ? ].