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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

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