9 files changed, 40 insertions, 1 deletions
diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out
new file mode 100644
index 0000000000..73da4f44f8
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure Foo.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v
new file mode 100644
index 0000000000..49597df6f7
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.v
@@ -0,0 +1,3 @@
+Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }.
+
+Canonical Structure Foo.
diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out
new file mode 100644
index 0000000000..63a2871b82
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure bar.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v
new file mode 100644
index 0000000000..10ee177aaf
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.v
@@ -0,0 +1,3 @@
+Definition bar := 99.
+
+Canonical Structure bar.
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.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d6d410d1ae..668b4e5788 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
 For pwrap: Argument scopes are [type_scope _]
 punwrap@{u} = 
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap)
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
new file mode 100644
index 0000000000..94a0b19118
--- /dev/null
+++ b/test-suite/output/optimize_heap.out
@@ -0,0 +1,8 @@
+1 subgoal
+  
+  ============================
+  True
+1 subgoal
+  
+  ============================
+  True
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
new file mode 100644
index 0000000000..e566bd7bab
--- /dev/null
+++ b/test-suite/output/optimize_heap.v
@@ -0,0 +1,7 @@
+(* optimize_heap should not affect the proof state *)
+
+Goal True.
+  idtac.
+  Show.
+  optimize_heap.
+  Show.