From 0e7ff6359c144c5ab4d7e16334c8ddc0d3078125 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Aug 2018 15:26:57 +0200
Subject: Fixing #7867 (class error message tries to print a "fun" with no
 binder).

---
 parsing/g_constr.mlg          | 2 +-
 test-suite/bugs/closed/7867.v | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/7867.v

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 49e1cd7ec9..7cb5af787b 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -249,7 +249,7 @@ GRAMMAR EXTEND Gram
 
   record_field_declaration:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
-      { (id, mkCLambdaN ~loc bl c) } ] ]
+      { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v
new file mode 100644
index 0000000000..d0c7902756
--- /dev/null
+++ b/test-suite/bugs/closed/7867.v
@@ -0,0 +1,4 @@
+(* Was a printer anomaly due to an internal lambda with no binders *)
+
+Class class := { foo : nat }.
+Fail Instance : class := { foo := 0 ; bar := 0 }.
-- 
cgit v1.2.3