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')

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')

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 58e804f07172acc6bb01c8bdafde1217eb4ec4b8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 13 Apr 2017 20:41:40 +0200
Subject: Reinstate fixpoint refolding in [cbn], deactivated by mistake.

Add a test-suite file to be sure we won't regress silently.
---
 test-suite/success/cbn.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/cbn.v

(limited to 'test-suite')

diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
new file mode 100644
index 0000000000..6aeb05f54e
--- /dev/null
+++ b/test-suite/success/cbn.v
@@ -0,0 +1,18 @@
+(* cbn is able to refold mutual recursive calls *)
+
+Fixpoint foo (n : nat) :=
+  match n with
+  | 0 => true
+  | S n => g n
+  end
+with g (n : nat) : bool :=
+  match n with
+  | 0 => true
+  | S n => foo n
+  end.
+Goal forall n, foo (S n) = g n.
+  intros. cbn.
+  match goal with
+    |- g _ = g _ => reflexivity
+  end.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From c98ed6692d16784e531f7eb8dbb1460fa20c7766 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 May 2017 11:13:31 +0200
Subject: Fix #5255: [Context (x : T := y)] should mean [Let x := y].

---
 test-suite/bugs/closed/5255.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/5255.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v
new file mode 100644
index 0000000000..5daaf9edbf
--- /dev/null
+++ b/test-suite/bugs/closed/5255.v
@@ -0,0 +1,24 @@
+Section foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End foo.
+
+Module Type Foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End Foo.
+
+Set Universe Polymorphism.
+
+Inductive unit := tt.
+Inductive eq {A} (x y : A) : Type := eq_refl : eq x y.
+
+Section bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End bar.
+
+Module Type Bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End Bar.
-- 
cgit v1.2.3


From 6735a7cbcaa3757e4d9ad60cb5a64fb5197b961e Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 17 May 2017 11:46:31 -0400
Subject: fix swapping of ids in tuples, bug 5486

---
 test-suite/bugs/closed/5486.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/5486.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v
new file mode 100644
index 0000000000..390133162f
--- /dev/null
+++ b/test-suite/bugs/closed/5486.v
@@ -0,0 +1,15 @@
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k :
+									 forall _ : T, Fm),
+    @eq Fm
+	(k
+	   match p return T with
+	   | pair p0 swap => fst p0
+	   end) f.
+  intros.
+  (* next statement failed in Bug 5486 *)
+  match goal with
+  | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ]
+    => pose (let (a, b) := d in e a b) as t0
+  end.
-- 
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/bugs/closed/5526.v    | 3 +++
 test-suite/output/Notations3.out | 4 ++++
 test-suite/output/Notations3.v   | 6 ++++++
 3 files changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/5526.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v
new file mode 100644
index 0000000000..88f219be30
--- /dev/null
+++ b/test-suite/bugs/closed/5526.v
@@ -0,0 +1,3 @@
+Fail Notation "x === x" := (eq_refl x) (at level 10).
+Reserved Notation "x === x" (only printing, at level 10).
+Notation "x === x" := (eq_refl x) (only printing).
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/Makefile        |  2 +-
 test-suite/output/Show.out | 12 ++++++++++++
 test-suite/output/Show.v   | 11 +++++++++++
 3 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/Show.out
 create mode 100644 test-suite/output/Show.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index c10cd4ed44..e87e133768 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -44,7 +44,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
 
 # read out an emacs config and look for coq-prog-args; if such exists, return it
 get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1)
-get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1)))))
+get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1))))
 SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
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')

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


From 1a169b01458829f9420aea9c855b1ef28e5c847d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 May 2017 22:34:57 +0200
Subject: Fixing a subtle bug in tclWITHHOLES.

This fixes Théo's bug on eset.
---
 test-suite/success/evars.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4e2bf45118..4b2f7b53e1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.
 Import EqNotations.
 Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a.
 
+(* Check that pre-existing evars are not counted as newly undefined in "set" *)
+(* Reported by Théo *)
 
+Goal exists n : nat, n = n -> True.
+eexists.
+set (H := _ = _).
+Abort.
-- 
cgit v1.2.3


From 2125c92aa9d17b27c9a19a59774e7e319e48262b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 29 May 2017 18:03:19 +0200
Subject: Omega: use "simpl" only on coefficents, not on atoms (fix #4132)

 Two issues in one:
  - some focused_simpl were called on the wrong locations
  - some focused_simpl were done on whole equations

 In the two cases, this could be bad if "simpl" goes too far
 with respect to what omega expects: later calls to "occurrence"
 might fail. This may happen for instance if an atom isn't a variable,
 but a let-in (b:=5:Z in the example).
---
 test-suite/bugs/closed/4132.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/bugs/closed/4132.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v
new file mode 100644
index 0000000000..806ffb771f
--- /dev/null
+++ b/test-suite/bugs/closed/4132.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(** bug 4132: omega was using "simpl" either on whole equations, or on
+   delimited but wrong spots. This was leading to unexpected reductions
+   when one atom (here [b]) is an evaluable reference instead of a variable. *)
+
+Lemma foo
+  (x y x' zxy zxy' z : Z)
+  (b := 5)
+  (Ry : - b <= y < b)
+  (Bx : x' <= b)
+  (H : - zxy' <= zxy)
+  (H' : zxy' <= x') : - b <= zxy.
+Proof.
+omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+Qed.
+
+Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "index out of bounds" in the past,
+          but I never managed to reproduce that in any version,
+          even before my fix. *)
+Qed.
+
+Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "Failure(occurence 2)" in the past,
+          but I never managed to reproduce that. *)
+Qed.
-- 
cgit v1.2.3


From e6c41b96a5ea9f8559acf176cdf997b05ccfb317 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 30 May 2017 12:10:35 +0200
Subject: Fix bug 5550: "typeclasses eauto with" does not work with section
 variables.

---
 test-suite/bugs/closed/5550.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5550.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v
new file mode 100644
index 0000000000..bb1222489a
--- /dev/null
+++ b/test-suite/bugs/closed/5550.v
@@ -0,0 +1,10 @@
+Section foo.
+
+  Variable bar : Prop.
+  Variable H : bar.
+
+  Goal bar.
+    typeclasses eauto with foobar.
+  Qed.
+
+End foo.
-- 
cgit v1.2.3


From 0bba5da999dc8eeef75c7040562f687ce589ed11 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 14:04:34 -0400
Subject: Add test-suite checks for coqchk with constraints

---
 test-suite/coqchk/univ.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 84a4009d7e..19eea94b19 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) :=
     (rank_injective : injective_in T natural D rank)
     (rank_onto :
        forall i, equivalent (less_than i n) (in_image T natural D rank i)).
+
+(* Constraints *)
+Universes i j.
+Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
+Constraint i < j.
+Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
+Universes i' j'.
+Constraint i' = j'.
+Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
+Inductive constraint4 : (Type -> Type) -> Type
+  := mk_constraint4 : let U1 := Type in
+                      let U2 := Type in
+                      constraint4 (fun x : U1 => (x : U2)).
-- 
cgit v1.2.3


From 4af77d01c434ff11f0899d504628f4ff91c49142 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 12:11:28 -0400
Subject: Add opened bug 5019

---
 test-suite/bugs/opened/5019.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/opened/5019.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v
new file mode 100644
index 0000000000..09622097c5
--- /dev/null
+++ b/test-suite/bugs/opened/5019.v
@@ -0,0 +1,4 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Fail Timeout 1 zify.
-- 
cgit v1.2.3


From 1d6a1036a7c472e1f20c5ec586d2484203a2fe2e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 12:48:47 -0400
Subject: Fix bug #5019 (looping zify on dependent types)

This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019),
"[zify] loops on dependent types"; before, we would see a `Z.of_nat (S
?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a
hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a
hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on
this.

This may not be the "right" fix (there may be cases where `zify` should
succeed where it still fails with this change), but this is a pure
bugfix in the sense that the only places where it changes the behavior
of `zify` are the places where, previously, `zify` looped forever.
---
 test-suite/bugs/closed/5019.v | 5 +++++
 test-suite/bugs/opened/5019.v | 4 ----
 2 files changed, 5 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/5019.v
 delete mode 100644 test-suite/bugs/opened/5019.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v
new file mode 100644
index 0000000000..7c973f88b5
--- /dev/null
+++ b/test-suite/bugs/closed/5019.v
@@ -0,0 +1,5 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Timeout 1 zify. (* used to loop forever; should take < 0.01 s *)
+Admitted.
diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v
deleted file mode 100644
index 09622097c5..0000000000
--- a/test-suite/bugs/opened/5019.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
-  clear; intros.
-  Fail Timeout 1 zify.
-- 
cgit v1.2.3


From a2e1e2fa4f0a005e07972488b6ce6ad59404bd2c Mon Sep 17 00:00:00 2001
From: Maxime Denes
Date: Fri, 9 Jun 2017 16:13:06 +0200
Subject: make test-suite/save-logs.sh usable also on old MacOS X

---
 test-suite/save-logs.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
index fb8a1c1b0a..b613621085 100755
--- a/test-suite/save-logs.sh
+++ b/test-suite/save-logs.sh
@@ -9,7 +9,7 @@ mkdir "$SAVEDIR"
 # keep this synced with test-suite/Makefile
 FAILMARK="==========> FAILURE <=========="
 
-FAILED=$(mktemp)
+FAILED=$(mktemp /tmp/coq-check-XXXXX)
 find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
 
 rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
-- 
cgit v1.2.3


From c054dda76825435019ad1b29f7f4292d937d98f9 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Tue, 30 May 2017 10:49:41 +0200
Subject: Add support for "-bypass-API" argument of "coq_makefile"

Plugin-writers can now use:

  -bypass-API

parameter with "coq_makefile".

The effect of that is that instead of

  -I API

the plugin will be compiled with:

  -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
---
 .../plugin-reach-outside-API-and-fail/run.sh       | 37 ++++++++++++++++++++++
 .../run.sh                                         | 32 +++++++++++++++++++
 test-suite/coq-makefile/template/src/test.ml4      |  1 +
 test-suite/coq-makefile/template/src/test_aux.ml   |  2 +-
 test-suite/coq-makefile/template/src/test_aux.mli  |  2 +-
 5 files changed, 72 insertions(+), 2 deletions(-)
 create mode 100755 test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
 create mode 100755 test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh

(limited to 'test-suite')

diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
new file mode 100755
index 0000000000..6301aa03c0
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+if make VERBOSE=1; then
+  # make command should have failed (but didn't)
+  exit 1
+else
+  # make command should have failed (and it indeed did)
+  exit 0
+fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
new file mode 100755
index 0000000000..991fb4a61d
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-bypass-API
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+make VERBOSE=1
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index 72765abe04..e7d0bfe1f8 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,3 +1,4 @@
+open API
 open Ltac_plugin
 DECLARE PLUGIN "test_plugin"
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index a01d0865a8..e134abd840 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = Proofview.tclUNIT ()
+let tac = API.Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 10020f27de..2e7ad1529f 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit Proofview.tactic
+val tac : unit API.Proofview.tactic
-- 
cgit v1.2.3