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").
---
 test-suite/output/ImplicitTypes.out | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite/output/ImplicitTypes.out')

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