Fixes #12322 (anomaly when printing "fun" binders with implicit types).

A pattern-matching clause was missing in 5f31403 (PR #11261).

The anomaly triggered in configurations like "fun (x:T) y => ..."
(even in the absence of "Implicit Types").

interp/constrextern.ml

@@ -836,7 +836,7 @@ let rec flatten_application c = match DAst.get c with
 
 let same_binder_type ty nal c =
   match nal, DAst.get c with
-  | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty'
+  | _::_, (GProd (_,_,ty',_) | GLambda (_,_,ty',_)) -> glob_constr_eq ty ty'
   | [], _ -> true
   | _ -> assert false
 

test-suite/output/ImplicitTypes.out

@@ -14,6 +14,12 @@ forall b1 b2, b1 = b2
      : Prop
 fun b => b = b
      : bool -> Prop
+fun b c : bool => b = c
+     : bool -> bool -> Prop
+fun c b : bool => b = c
+     : bool -> bool -> Prop
+fun b1 b2 => b1 = b2
+     : bool -> bool -> Prop
 fix f b (n : nat) {struct n} : bool :=
   match n with
   | 0 => b

test-suite/output/ImplicitTypes.v

@@ -23,6 +23,9 @@ Check forall b1 b2, b1 = b2.
 
 (* Check in "fun" *)
 Check fun b => b = b.
+Check fun b c => b = c.
+Check fun c b => b = c.
+Check fun b1 b2 => b1 = b2.
 
 (* Check in binders *)
 Check fix f b n := match n with 0 => b | S p => f b p end.