From 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 23 Sep 2017 12:25:35 +0200
Subject: Fixing a bug of Print for inductive types with let-ins in parameters.

Adding a "let-in"-sensitive function hnf_prod_applist_assum to
instantiate parameters and using it for printing.

Thanks to PMP for reporting.
---
 test-suite/output/Inductive.out | 4 ++++
 test-suite/output/Inductive.v   | 4 ++++
 2 files changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e912003f03..af202ea01c 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,3 +1,7 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+
+For foo: Argument scopes are [type_scope _]
+For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 8db8956e32..8ff91268a6 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -1,3 +1,7 @@
 Fail Inductive list' (A:Set) : Set :=
 | nil' : list' A
 | cons' : A -> list' A -> list' (A*A).
+
+(* Check printing of let-ins *)
+Inductive foo (A : Type) (x : A) (y := x) := Foo.
+Print foo.
-- 
cgit v1.2.3