6 files changed, 51 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5eb8a88698..d6ba84d0bf 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -232,7 +232,17 @@ let occur_rigidly flags env evd (evk,_) t =
 let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let open ValuePattern in
   let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
+  let t2, sk2' = decompose_app_vect sigma (shrink_eta env t2) in
+  let sk2 = Stack.append_app sk2' sk2 in
   let (sigma, solution), sk2_effective =
+    let t2 =
+      let rec remove_lambda t2 =
+        match EConstr.kind sigma t2 with
+        | Lambda (_,_,t2) -> remove_lambda t2
+        | Cast (t2,_,_) -> remove_lambda t2
+        | App (t2,_) -> t2
+        | _ -> t2 in
+      if Stack.is_empty sk2 then remove_lambda t2 else t2 in
     try
       match EConstr.kind sigma t2 with
         Prod (_,a,b) -> (* assert (l2=[]); *)
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
index 3ef6e98373..145663d3b9 100644
--- a/pretyping/structures.ml
+++ b/pretyping/structures.ml
@@ -161,6 +161,7 @@ let rec of_constr env t =
     let patt, n, args = of_constr env f in
     patt, n, args @ Array.to_list vargs
   | Rel n -> Default_cs, Some n, []
+  | Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
   | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
@@ -222,6 +223,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
   let lpj = keep_true_projections lpj in
   let nenv = Termops.push_rels_assum sign env in
   List.fold_left2 (fun acc (spopt, canonical) t ->
+      let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in
       if canonical
       then
         Option.cata (fun proji_sp ->
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.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index d8eb005ab2..72e6e757d3 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -297,7 +297,6 @@ Require Import ssreflect ssrfun.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Set Warnings "-projection-no-head-constant".
 
 Notation reflect := Bool.reflect.
 Notation ReflectT := Bool.ReflectT.
@@ -1227,7 +1226,9 @@ Definition clone_pred T U :=
 Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope.
 
 Canonical predPredType T := PredType (@id (pred T)).
+Set Warnings "-redundant-canonical-projection".
 Canonical boolfunPredType T := PredType (@id (T -> bool)).
+Set Warnings "redundant-canonical-projection".
 
 (** The type of abstract collective predicates.
  While {pred T} is contertible to pred T, it presents the pred_sort coercion