1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 885fff4836..c0065809db 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -80,3 +80,10 @@ Record DecidableOrder : Type :=
 ; le_trans : transitive _ le
 ; le_total : forall x y, {x <= y}+{y <= x}
 }.
+
+(* Test syntactic sugar suggested by wish report #2138 *)
+
+Record R : Type := {
+  P (A : Type) : Prop := exists x : A -> A, x = x;
+  Q A : P A -> P A
+}.