From 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser
Date: Thu, 14 May 2020 17:08:20 +0200
Subject: Enable canonical `fun _ => _` projections.

---
 test-suite/output/Warnings.out          |  5 +++--
 test-suite/output/Warnings.v            |  4 ++--
 test-suite/success/CanonicalStructure.v | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 37 insertions(+), 4 deletions(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3