From 495bccc436cfe72af9955b4b9d8564a8831850b9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:23:53 +0100
Subject: Fixing #4499 (not using unnamed record field in {| |} notation).

---
 test-suite/output/Record.out | 6 ++++++
 test-suite/output/Record.v   | 5 +++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 36d643a447..37b4fb25f7 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -14,3 +14,9 @@ build 5
      : test_r
 build_c 5
      : test_c
+fun '(C _ p) => p
+     : N -> True
+fun '{| T := T |} => T
+     : N -> Type
+fun '(C T p) => (T, p)
+     : N -> Type * True
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 6aa3df9830..c3d9f1e573 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -19,3 +19,8 @@ Check build 5.
 Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
+
+Record N := C { T : Type; _ : True }.
+Check fun x:N => let 'C _ p := x in p.
+Check fun x:N => let 'C T _ := x in T.
+Check fun x:N => let 'C T p := x in (T,p).
-- 
cgit v1.2.3


From f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:59:04 +0100
Subject: Better support for printing constructors with let-ins.

This allows e.g. to use the record notations even when there are
defined fields.

A priori fixed also missing parameters when interpreting primitive
tokens.
---
 test-suite/output/Cases.out  | 14 +++++++++++---
 test-suite/output/Cases.v    | 15 +++++++++++++++
 test-suite/output/Record.out | 10 ++++++++++
 test-suite/output/Record.v   |  7 +++++++
 4 files changed, 43 insertions(+), 3 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 8ce6f9795c..f064dfe763 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,18 +2,18 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | @k _ x0 => f x0 (F x0)
+  | k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
 Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
 proj = 
@@ -72,3 +72,11 @@ e1 : texp t1
 e2 : texp t2
 The term "0" has type "nat" while it is expected to have type
  "typeDenote t0".
+fun '{{n, m, _}} => n + m
+     : J -> nat
+fun '{{n, m, p}} => n + m + p
+     : J -> nat
+fun '(D n m p q) => n + m + p + q
+     : J -> nat
+The command has indeed failed with message:
+The constructor D (in type J) expects 3 arguments.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4074896420..6a4fd007df 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
   | TBinop t1 t2 _ b e1 e2 => O
   end.
 
+(* Test notations with local definitions in constructors *)
+
+Inductive J := D : forall n m, let p := n+m in nat -> J.
+Notation "{{ n , m , q }}" := (D n m q).
+
+Check fun x : J => let '{{n, m, _}} := x in n + m.
+Check fun x : J => let '{{n, m, p}} := x in n + m + p.
+
+(* Cannot use the notation because of the dependency in p *)
+
+Check fun x => let '(D n m p q) := x in n+m+p+q.
+
+(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
+
+Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 37b4fb25f7..d45343fe60 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -20,3 +20,13 @@ fun '{| T := T |} => T
      : N -> Type
 fun '(C T p) => (T, p)
      : N -> Type * True
+fun '{| q := p |} => p
+     : M -> True
+fun '{| U := T |} => T
+     : M -> Type
+fun '{| U := T; q := p |} => (T, p)
+     : M -> Type * True
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index c3d9f1e573..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -24,3 +24,10 @@ Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
 Check fun x:N => let 'C T p := x in (T,p).
+
+Record M := D { U : Type; a := 0; q : True }.
+Check fun x:M => let 'D T _ p := x in p.
+Check fun x:M => let 'D T _ p := x in T.
+Check fun x:M => let 'D T p := x in (T,p).
+Check fun x:M => let 'D T a p := x in (T,p,a).
+Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
-- 
cgit v1.2.3


From 8c2c92cf47536b93e8e7377e8cfd89342325dbcc Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 17 May 2017 12:59:08 -0400
Subject: Fixing bug #5526,allow nonlinear variables in Notation patterns

---
 test-suite/output/Notations3.out | 4 ++++
 test-suite/output/Notations3.v   | 6 ++++++
 2 files changed, 10 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 360f379676..0cb870c577 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,3 +98,7 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
 tele (t : Type) '(y, z) (x : t0) := tt
      : forall t : Type, nat * nat -> t -> fpack
+fun x : ?A => x === x
+     : forall x : ?A, x = x
+where
+?A : [x : ?A |- Type] (x cannot be used)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 4b8bfe3124..5676fe8c7c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" :=
   (at level 85, x binder, z binder).
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
+
+(**********************************************************************)
+(* Test printing of #5526                                             *)
+
+Notation "x === x" := (eq_refl x) (only printing, at level 10).
+Check (fun x => eq_refl x).
-- 
cgit v1.2.3


From 92e3fddf3b2b169e4853cb382f5c44d7ec9f2733 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 19 May 2017 11:41:28 -0400
Subject: add test for Show with -emacs, bug 5535

---
 test-suite/output/Show.out | 12 ++++++++++++
 test-suite/output/Show.v   | 11 +++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 test-suite/output/Show.out
 create mode 100644 test-suite/output/Show.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
new file mode 100644
index 0000000000..d0c963be17
--- /dev/null
+++ b/test-suite/output/Show.out
@@ -0,0 +1,12 @@
+3 subgoals, subgoal 1 (ID 29)
+  
+  H : 0 = 0
+  ============================
+  1 = 1
+
+subgoal 2 (ID 33) is:
+ 1 = S (S m')
+subgoal 3 (ID 20) is:
+ S (S n') = S m
+(dependent evars: (printing disabled) )
+
diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v
new file mode 100644
index 0000000000..60faac8dd9
--- /dev/null
+++ b/test-suite/output/Show.v
@@ -0,0 +1,11 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
+
+(* tests of Show output with -emacs flag to coqtop; see bug 5535 *)
+
+Theorem nums : forall (n m : nat), n = m -> (S n) = (S m).
+Proof.
+  intros.
+  induction n as [| n'].  
+  induction m as [| m'].
+  Show.
+Admitted.
-- 
cgit v1.2.3


From ec57e7bedbd6719ad1b03800d6a8d7efd1b75ee4 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Thu, 25 May 2017 11:03:18 -0400
Subject: Bug 5546, qualify datatype constructors when needed

---
 test-suite/output/ShowMatch.out |  8 ++++++++
 test-suite/output/ShowMatch.v   | 13 +++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test-suite/output/ShowMatch.out
 create mode 100644 test-suite/output/ShowMatch.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out
new file mode 100644
index 0000000000..e5520b8dfa
--- /dev/null
+++ b/test-suite/output/ShowMatch.out
@@ -0,0 +1,8 @@
+match # with
+ | f =>
+ end
+ 
+match # with
+ | A.f =>
+ end
+ 
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
new file mode 100644
index 0000000000..02b7eada83
--- /dev/null
+++ b/test-suite/output/ShowMatch.v
@@ -0,0 +1,13 @@
+(* Bug 5546 complained about unqualified constructors in Show Match output, 
+   when qualification is needed to disambiguate them
+*)
+
+Module A.
+  Inductive foo := f.
+  Show Match foo. (* no need to disambiguate *)
+End A. 
+
+Module B.
+  Inductive foo := f.
+  (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
+  Show Match A.foo. 
-- 
cgit v1.2.3