From 6a85fd439ed9051d0ae87fe134d223ccd1bd94ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 May 2020 07:24:53 +0200
Subject: Fixes #12322 (anomaly when printing "fun" binders with implicit
 types).

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

The anomaly triggered in configurations like "fun (x:T) y => ..."
(even in the absence of "Implicit Types").
---
 interp/constrextern.ml              | 2 +-
 test-suite/output/ImplicitTypes.out | 6 ++++++
 test-suite/output/ImplicitTypes.v   | 3 +++
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5a5bde616..ddf304c37c 100644
--- a/interp/constrextern.ml
+++ b/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
 
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
index 824c260e92..42cb2309e0 100644
--- a/test-suite/output/ImplicitTypes.out
+++ b/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
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
index dbc83f9229..205c6a67bf 100644
--- a/test-suite/output/ImplicitTypes.v
+++ 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.
-- 
cgit v1.2.3


From 6b793e6b39b60cef8c3163cb6cd240e5a0ecbfc5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 May 2020 07:35:59 +0200
Subject: Add changelog for #12323.

---
 .../12323-master+fix12322-anomaly-implicit-binder-factorization.rst   | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst

diff --git a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst b/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
new file mode 100644
index 0000000000..e5ec865b15
--- /dev/null
+++ b/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Anomaly possibly raised when printing binders with implicit types
+  (`#12323 <https://github.com/coq/coq/pull/12323>`_,
+  by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).
-- 
cgit v1.2.3