Enable canonical `fun _ => _` projections.

3 files changed, 37 insertions, 4 deletions

diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
index a70f8ca45a..23119bab97 100644
--- a/test-suite/output/Warnings.out
+++ b/test-suite/output/Warnings.out
@@ -1,3 +1,4 @@
 File "stdin", line 4, characters 0-22:
-Warning: Projection value has no head constant: fun x : B => x in canonical
-instance a of b, ignoring it. [projection-no-head-constant,typechecker]
+Warning: Projection value has no head constant: forall x : nat, x > 0 in
+canonical instance a of b, ignoring it.
+[projection-no-head-constant,typechecker]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 7465442cab..ce92bcbbb2 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-Record A := { B:Type; b:B->B }.
-Definition a B := {| B:=B; b:=fun x => x |}.
+Record A := { B:Type; b:Prop }.
+Definition a B := {| B:=B; b:=forall x, x > 0 |}.
 Canonical Structure a.
 
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 88702a6e80..a833dd0bd6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -70,3 +70,35 @@ Section W.
   Check (refl_equal _ : l _ = x2).
 End W.
 Fail Check (refl_equal _ : l _ = x2).
+
+(* Lambda keys *)
+Section L1.
+  Structure cs_lambda := { cs_lambda_key : nat -> nat }.
+  #[local] Canonical Structure cs_lambda_func :=
+    {| cs_lambda_key := fun x => x + 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _).
+End L1.
+
+Section L2.
+  #[local] Canonical Structure cs_lambda_func2 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L2.
+
+Section L3.
+  #[local] Canonical Structure cs_lambda_func3 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L3.
+
+Section L4.
+  #[local] Canonical Structure cs_lambda_func4 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L4.
+
+Section L5.
+  #[local] Canonical Structure cs_lambda_func5 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L5.