summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2928.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2928.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2928.v11
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v
new file mode 100644
index 00000000..21e92ae2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2928.v
@@ -0,0 +1,11 @@
+Class Equiv A := equiv: A -> A -> Prop.
+Infix "=" := equiv : type_scope.
+
+Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
+
+Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
+
+Class SemiLattice A op `{Equiv A} :=
+ { semilattice_sg :>> SemiGroup A op
+ ; redundant : Associative op
+ }.