From 70650127254e8122252e6c7201d4d835320a5585 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 31 Mar 2019 20:06:30 +0200
Subject: Remove test file with Timeout that failed spuriously.

See https://gitlab.com/coq/coq/-/jobs/187496964
---
 test-suite/bugs/closed/bug_4429.v | 31 -------------------------------
 1 file changed, 31 deletions(-)
 delete mode 100644 test-suite/bugs/closed/bug_4429.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v
deleted file mode 100644
index bf0e570ab8..0000000000
--- a/test-suite/bugs/closed/bug_4429.v
+++ /dev/null
@@ -1,31 +0,0 @@
-Require Import Arith.Compare_dec.
-Require Import Unicode.Utf8.
-
-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
-  match n with
-    | O    => x
-    | S n' => f (my_nat_iter n' f x)
-  end.
-
-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
-  match mn with
-    | (0, 0)       => 0
-    | (0, S n')    => S n'
-    | (S m', 0)    => S m'
-    | (S m', S n') =>
-      match le_gt_dec (S m') (S n') with
-        | left  _ => f (S m', S n' - S m')
-        | right _ => f (S m' - S n', S n')
-      end
-  end.
-
-Axiom max_correct_l : ∀ m n : nat, m <= max m n.
-Axiom max_correct_r : ∀ m n : nat, n <= max m n.
-
-Hint Resolve max_correct_l max_correct_r : arith.
-
-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
-Proof.
-  intros.
-  Timeout 3 eauto with arith.
-Qed.
-- 
cgit v1.2.3


From 53438d636ddd4f05249ef13e89306759bfe3499f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 28 Apr 2019 15:21:00 +0200
Subject: [test-suite] Remove a test with a Timeout that fails frequently on
 CI.

---
 test-suite/success/ROmega3.v | 35 -----------------------------------
 1 file changed, 35 deletions(-)
 delete mode 100644 test-suite/success/ROmega3.v

(limited to 'test-suite')

diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
deleted file mode 100644
index ef9cb17b4b..0000000000
--- a/test-suite/success/ROmega3.v
+++ /dev/null
@@ -1,35 +0,0 @@
-
-Require Import ZArith Lia.
-Local Open Scope Z_scope.
-
-(** Benchmark provided by Chantal Keller, that romega used to
-    solve far too slowly (compared to omega or lia). *)
-
-(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated.
-   The tests in this file remain but now call the `lia` tactic. *)
-
-
-Parameter v4 : Z.
-Parameter v3 : Z.
-Parameter o4 : Z.
-Parameter s5 : Z.
-Parameter v2 : Z.
-Parameter o5 : Z.
-Parameter s6 : Z.
-Parameter v1 : Z.
-Parameter o6 : Z.
-Parameter s7 : Z.
-Parameter v0 : Z.
-Parameter o7 : Z.
-
-Lemma lemma_5833 :
- ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
-      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
-         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192
-\/
-  16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
-      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
-         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
-Proof.
-Timeout 1 lia. (* should take a few milliseconds, not seconds *)
-Timeout 1 Qed. (* ditto *)
-- 
cgit v1.2.3


From af3673b08204cb4d3d6994aa3a5bd6363bfd7459 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 17 Jan 2019 11:44:38 +0000
Subject: Fix #9344, #9348: incorrect unsafe to_constr in vnorm

---
 test-suite/bugs/closed/bug_9344.v | 1 +
 test-suite/bugs/closed/bug_9348.v | 3 +++
 2 files changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9344.v
 create mode 100644 test-suite/bugs/closed/bug_9348.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_9344.v b/test-suite/bugs/closed/bug_9344.v
new file mode 100644
index 0000000000..fbf86b2dad
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9344.v
@@ -0,0 +1 @@
+Compute _ I.
diff --git a/test-suite/bugs/closed/bug_9348.v b/test-suite/bugs/closed/bug_9348.v
new file mode 100644
index 0000000000..a4673b5ffc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9348.v
@@ -0,0 +1,3 @@
+Set Primitive Projections.
+Record r {A} := R {f : A -> A}.
+Compute f _ I.
-- 
cgit v1.2.3


From ace68d056551a4a2834d1d4908375dba7a1fbc44 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 29 Apr 2019 17:35:06 +0200
Subject: Fix variant of #9344 for native_compute

---
 test-suite/bugs/closed/bug_9344.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_9344.v b/test-suite/bugs/closed/bug_9344.v
index fbf86b2dad..0d44c9721a 100644
--- a/test-suite/bugs/closed/bug_9344.v
+++ b/test-suite/bugs/closed/bug_9344.v
@@ -1 +1,2 @@
 Compute _ I.
+Eval native_compute in _ I.
-- 
cgit v1.2.3


From 7875955f513f55c1fcef90becdaaa572baa3e5ae Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Wed, 24 Apr 2019 23:02:08 +0200
Subject: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType`
 interface

** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
**  Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result  `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large  `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.
---
 test-suite/prerequisite/ssr_mini_mathcomp.v |  4 ++--
 test-suite/ssr/nonPropType.v                | 23 +++++++++++++++++++++++
 test-suite/ssr/predRewrite.v                | 28 ++++++++++++++++++++++++++++
 3 files changed, 53 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/ssr/nonPropType.v
 create mode 100644 test-suite/ssr/predRewrite.v

(limited to 'test-suite')

diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index ca360f65a7..6fc630056c 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -634,9 +634,9 @@ Fixpoint mem_seq (s : seq T) :=
 
 Definition eqseq_class := seq T.
 Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
-Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
+Coercion pred_of_eq_seq (s : eqseq_class) : {pred T} := [eta mem_seq s].
 
-Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+Canonical seq_predType := @PredType T (seq T) pred_of_eq_seq.
 
 Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
 
diff --git a/test-suite/ssr/nonPropType.v b/test-suite/ssr/nonPropType.v
new file mode 100644
index 0000000000..bcdc907b38
--- /dev/null
+++ b/test-suite/ssr/nonPropType.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+(** Test the nonPropType interface and its application to prevent unwanted
+    instantiations in views. **)
+
+Lemma raw_flip {T} (x y : T) : x = y -> y = x. Proof. by []. Qed.
+Lemma flip {T : nonPropType} (x y : T) : x = y -> y = x. Proof. by []. Qed.
+
+Lemma testSet : true = false -> True.
+Proof.
+Fail move/raw_flip.
+have flip_true := @flip _ true.
+(* flip_true : forall y : notProp bool, x = y -> y = x *)
+simpl in flip_true.
+(* flip_true : forall y : bool, x = y -> y = x *)
+by move/flip.
+Qed.
+
+Lemma override (t1 t2 : True) : t1 = t2 -> True.
+Proof.
+Fail move/flip.
+by move/(@flip (notProp True)).
+Qed.
diff --git a/test-suite/ssr/predRewrite.v b/test-suite/ssr/predRewrite.v
new file mode 100644
index 0000000000..2ad762ccf1
--- /dev/null
+++ b/test-suite/ssr/predRewrite.v
@@ -0,0 +1,28 @@
+Require Import ssreflect ssrfun ssrbool.
+
+(** Test the various idioms that control rewriting in boolean predicate. **)
+
+Definition simpl_P := [pred a | ~~ a].
+Definition nosimpl_P : pred bool := [pred a | ~~ a].
+Definition coll_P : collective_pred bool := [pred a | ~~ a].
+Definition appl_P : applicative_pred bool := [pred a | ~~ a].
+Definition can_appl_P : pred bool := [pred a | ~~ a].
+Canonical register_can_appl_P := ApplicativePred can_appl_P.
+Ltac see_neg := (let x := fresh "x" in set x := {-}(~~ _); clear x).
+
+Lemma test_pred_rewrite (f := false) : True.
+Proof.
+have _: f \in simpl_P by rewrite inE; see_neg.
+have _ a: simpl_P (a && f) by simpl; see_neg; rewrite andbF.
+have _ a: simpl_P (a && f) by rewrite inE; see_neg; rewrite andbF.
+have _: f \in nosimpl_P by rewrite inE; see_neg.
+have _: nosimpl_P f. simpl. Fail see_neg. Fail rewrite inE. done.
+have _: f \in coll_P. Fail rewrite inE. by rewrite in_collective; see_neg.
+have _: f \in appl_P.
+  rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
+  Fail rewrite app_predE. done.
+have _: f \in can_appl_P.
+  rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
+  by rewrite app_predE in_simpl; see_neg.
+done.
+Qed.
-- 
cgit v1.2.3


From 7fbb53b1649627b3f765fc9516becd3cd1674464 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 29 Apr 2019 20:05:58 +0200
Subject: Mini-test.

---
 test-suite/success/change.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index a9821b027f..5a8f735151 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -68,3 +68,11 @@ eassumption.
 match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
 match goal with |- 0+1=1 => trivial end.
 Qed.
+
+(* Mini-check that no_check does not check *)
+
+Goal False.
+change_no_check True.
+exact I.
+Fail Qed.
+Abort.
-- 
cgit v1.2.3


From d9a975352e5982602d3315facfa005ea40b16bcb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 30 Apr 2019 21:48:34 +0200
Subject: Remove leftover test suite file Quote.out

---
 test-suite/output/Quote.out | 24 ------------------------
 1 file changed, 24 deletions(-)
 delete mode 100644 test-suite/output/Quote.out

(limited to 'test-suite')

diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
deleted file mode 100644
index 998eb37cc8..0000000000
--- a/test-suite/output/Quote.out
+++ /dev/null
@@ -1,24 +0,0 @@
-(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx))
-(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-   (f_and (f_const A)
-      (f_and (f_or (f_atom End_idx) (f_const A))
-         (f_or (f_const A) (f_not (f_atom End_idx))))))
-1 subgoal
-  
-  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
-      B
-  ============================
-  interp_f
-    (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
-    (f_and (f_atom (Left_idx End_idx))
-       (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
-          (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
-1 subgoal
-  
-  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
-      B
-  ============================
-  interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-    (f_and (f_const A)
-       (f_and (f_or (f_atom End_idx) (f_const A))
-          (f_or (f_const A) (f_not (f_atom End_idx)))))
-- 
cgit v1.2.3


From afb58502f900554986aeee9a749871630f117edd Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 10:44:56 +0200
Subject: Test case for #5752

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_5752.v b/test-suite/bugs/closed/bug_5752.v
new file mode 100644
index 0000000000..b4218d66df
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5752.v
@@ -0,0 +1,8 @@
+Class C (A : Type) := c : A.
+
+Hint Mode C ! : typeclass_instances.
+
+Goal forall f : (forall A, C A -> C (list A)), True.
+intros.
+  Check c. (* Loops if modes are ignored. *)
+Abort.
-- 
cgit v1.2.3


From 24c570834dccc90c7ff14d3f6b9d33b818fa79c9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Apr 2019 18:50:47 +0200
Subject: Fix #9994: `revert dependent` is extremely slow.

We add a fast path when generalizing over variables.
---
 test-suite/bugs/closed/bug_10025.v | 39 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10025.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v
new file mode 100644
index 0000000000..1effc771b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10025.v
@@ -0,0 +1,39 @@
+Require Import Program.
+
+Axiom I : Type.
+
+Inductive S : Type := NT : I -> S.
+
+Axiom F : S -> Type.
+
+Axiom G : forall (s : S), F s -> Type.
+
+Section S.
+
+Variable init : I.
+Variable my_s : F (NT init).
+
+Inductive foo : forall (s: S) (hole_sem: F s), Type :=
+| Foo : foo (NT init) my_s.
+
+Goal forall
+  (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit),
+match
+  match x with tt => tt end
+with
+| tt =>
+    match
+      match ptz in foo x s return (forall _ : G x s, unit) with
+      | Foo => fun _ : G (NT init) my_s => tt
+      end pt
+    with
+    | tt => False
+    end
+end.
+Proof.
+dependent destruction ptz.
+(* Check well-typedness of goal *)
+match goal with [ |- ?P ] => let t := type of P in idtac end.
+Abort.
+
+End S.
-- 
cgit v1.2.3


From dd60b4a292b870e08c23ddcb363630cbb2ed1227 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 May 2019 08:16:37 +0200
Subject: [primitive integers] Make div21 implems consistent with its
 specification

There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v

* comment the implementations with loop invariants to enable an easy
  pen&paper proof of correctness (note to reviewers: the one in
  uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
  (only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
  (cmp is computed at the end of the first loop rather than at the beginning,
   potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
  new specifiation of div21
* add a test
---
 test-suite/arithmetic/diveucl_21.v | 8 ++++++++
 test-suite/bugs/closed/bug_10031.v | 9 +++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10031.v

(limited to 'test-suite')

diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
index 7e12a08906..b888c97be3 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/arithmetic/diveucl_21.v
@@ -15,3 +15,11 @@ Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (46116860184273879
 Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
 Definition compute2 := Eval compute in diveucl_21 3 1 2.
 Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
+
+Check (eq_refl : diveucl_21 1 1 0 = (0,0)).
+Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)).
+Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)).
+
+Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)).
+Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)).
+Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)).
diff --git a/test-suite/bugs/closed/bug_10031.v b/test-suite/bugs/closed/bug_10031.v
new file mode 100644
index 0000000000..15b53de00d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10031.v
@@ -0,0 +1,9 @@
+Require Import Int63 ZArith.
+
+Open Scope int63_scope.
+
+Goal False.
+cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z));
+  [discriminate| ].
+Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec).
+Abort.
-- 
cgit v1.2.3


From a0cfcc318919b315b142abab7604f04e8dd6420f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 May 2019 21:27:19 +0200
Subject: Tactics: fixing "change_no_check in".

(Merge of the initial version with #9983 was broken)
---
 test-suite/success/change.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5a8f735151..2f676cf9ad 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -71,8 +71,13 @@ Qed.
 
 (* Mini-check that no_check does not check *)
 
-Goal False.
-change_no_check True.
-exact I.
+Goal True -> False.
+intro H.
+change_no_check nat.
+apply S.
+change_no_check nat with bool.
+change_no_check nat in H.
+change_no_check nat with (bool->bool) in H.
+exact (H true).
 Fail Qed.
 Abort.
-- 
cgit v1.2.3


From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 14:09:42 +0200
Subject: Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
---
 test-suite/Makefile            |   5 +-
 test-suite/ltac2/compat.v      |  58 +++++++++
 test-suite/ltac2/errors.v      |  12 ++
 test-suite/ltac2/example1.v    |  27 ++++
 test-suite/ltac2/example2.v    | 281 +++++++++++++++++++++++++++++++++++++++++
 test-suite/ltac2/matching.v    |  71 +++++++++++
 test-suite/ltac2/quot.v        |  26 ++++
 test-suite/ltac2/rebind.v      |  34 +++++
 test-suite/ltac2/stuff/ltac2.v | 143 +++++++++++++++++++++
 test-suite/ltac2/tacticals.v   |  34 +++++
 test-suite/ltac2/typing.v      |  72 +++++++++++
 11 files changed, 761 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/ltac2/compat.v
 create mode 100644 test-suite/ltac2/errors.v
 create mode 100644 test-suite/ltac2/example1.v
 create mode 100644 test-suite/ltac2/example2.v
 create mode 100644 test-suite/ltac2/matching.v
 create mode 100644 test-suite/ltac2/quot.v
 create mode 100644 test-suite/ltac2/rebind.v
 create mode 100644 test-suite/ltac2/stuff/ltac2.v
 create mode 100644 test-suite/ltac2/tacticals.v
 create mode 100644 test-suite/ltac2/typing.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index ba591ede20..94011447d7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -99,7 +99,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr arithmetic
+  coqdoc ssr arithmetic ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -181,6 +181,7 @@ summary:
 	  $(call summary_dir, "tools/ tests", tools); \
 	  $(call summary_dir, "Unit tests", unit-tests); \
 	  $(call summary_dir, "Machine arithmetic tests", arithmetic); \
+	  $(call summary_dir, "Ltac2 tests", ltac2); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -319,7 +320,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
new file mode 100644
index 0000000000..489fa638e4
--- /dev/null
+++ b/test-suite/ltac2/compat.v
@@ -0,0 +1,58 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+(** Test calls to Ltac1 from Ltac2 *)
+
+Ltac2 foo () := ltac1:(discriminate).
+
+Goal true = false -> False.
+Proof.
+foo ().
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(rewrite H); reflexivity.
+Abort.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac2 bar nay := ltac1:(discriminate nay).
+
+Fail Ltac2 pose1 (v : constr) :=
+  ltac1:(pose $v).
+
+(** Test calls to Ltac2 from Ltac1 *)
+
+Set Default Proof Mode "Classic".
+
+Ltac foo := ltac2:(foo ()).
+
+Goal true = false -> False.
+Proof.
+ltac2:(foo ()).
+Qed.
+
+Goal true = false -> False.
+Proof.
+foo.
+Qed.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac bar x := ltac2:(foo x).
+
+Ltac mytac tac := idtac "wow".
+
+Goal True.
+Proof.
+(** Fails because quotation is evaluated eagerly *)
+Fail mytac ltac2:(fail).
+(** One has to thunk thanks to the idtac trick *)
+let t := idtac; ltac2:(fail) in mytac t.
+constructor.
+Qed.
diff --git a/test-suite/ltac2/errors.v b/test-suite/ltac2/errors.v
new file mode 100644
index 0000000000..c677f6af5d
--- /dev/null
+++ b/test-suite/ltac2/errors.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Goal True.
+Proof.
+let x := Control.plus
+  (fun () => let _ := constr:(nat -> 0) in 0)
+  (fun e => match e with Not_found => 1 | _ => 2 end) in
+match Int.equal x 2 with
+| true => ()
+| false => Control.throw (Tactic_failure None)
+end.
+Abort.
diff --git a/test-suite/ltac2/example1.v b/test-suite/ltac2/example1.v
new file mode 100644
index 0000000000..023791050f
--- /dev/null
+++ b/test-suite/ltac2/example1.v
@@ -0,0 +1,27 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Control.
+
+(** Alternative implementation of the hyp primitive *)
+Ltac2 get_hyp_by_name x :=
+  let h := hyps () in
+  let rec find x l := match l with
+  | [] => zero Not_found
+  | p :: l =>
+    match p with
+    | (id, _, t) =>
+      match Ident.equal x id with
+      | true => t
+      | false => find x l
+      end
+    end
+  end in
+  find x h.
+
+Print Ltac2 get_hyp_by_name.
+
+Goal forall n m, n + m = 0 -> n = 0.
+Proof.
+refine (fun () => '(fun n m H => _)).
+let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
+Abort.
diff --git a/test-suite/ltac2/example2.v b/test-suite/ltac2/example2.v
new file mode 100644
index 0000000000..c953d25061
--- /dev/null
+++ b/test-suite/ltac2/example2.v
@@ -0,0 +1,281 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Set Default Goal Selector "all".
+
+Goal exists n, n = 0.
+Proof.
+split with (x := 0).
+reflexivity.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+split with 0.
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+let myvar := Std.NamedHyp @x in split with ($myvar := 0).
+split.
+Qed.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+intros H.
+eelim &H.
+split.
+Qed.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+intros H.
+elim &H with 0.
+split.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+Fail apply &H.
+apply &H with (m := 0).
+split.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0.
+Proof.
+intros P H e.
+apply &H with (m := 1) in e.
+exact e.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+eapply &H.
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+Fail constructor 1.
+constructor 1 with (x := 0).
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+econstructor 1.
+split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+induction &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+destruct &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall b1 b2, andb b1 b2 = andb b2 b1.
+Proof.
+intros b1 b2.
+destruct &b1 as [|], &b2 as [|]; split.
+Qed.
+
+Goal forall n m, n = 0 -> n + m = m.
+Proof.
+intros n m Hn.
+rewrite &Hn; split.
+Qed.
+
+Goal forall n m p, n = m -> p = m -> 0 = n -> p = 0.
+Proof.
+intros n m p He He' Hn.
+rewrite &He, <- &He' in Hn.
+rewrite &Hn.
+split.
+Qed.
+
+Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0.
+Proof.
+intros n m He He' He''.
+rewrite <- &He by assumption.
+Control.refine (fun () => &He'').
+Qed.
+
+Goal forall n (r := if true then n else 0), r = n.
+Proof.
+intros n r.
+hnf in r.
+split.
+Qed.
+
+Goal 1 = 0 -> 0 = 0.
+Proof.
+intros H.
+pattern 0 at 1.
+let occ := 2 in pattern 1 at 1, 0 at $occ in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+native_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2 - 0 -> True.
+Proof.
+intros H.
+vm_compute plus in H.
+reflexivity.
+Qed.
+
+Goal 1 = 0 -> True /\ True.
+Proof.
+intros H.
+split; fold (1 + 0) (1 + 0) in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+cbv [ Nat.add ].
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+let x := reference:(Nat.add) in
+cbn beta iota delta [ $x ].
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+simpl beta.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+lazy.
+reflexivity.
+Qed.
+
+Goal let x := 1 + 1 - 1 in x = x.
+Proof.
+intros x.
+unfold &x at 1.
+let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
+reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+exists 0, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+eexists _, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+refine '(let x := 0 in _).
+eexists; exists &x; reflexivity.
+Qed.
+
+Goal True.
+Proof.
+pose (X := True).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+pose True as X.
+constructor.
+Qed.
+
+Goal True.
+Proof.
+let x := @foo in
+set ($x := True) in * |-.
+constructor.
+Qed.
+
+Goal 0 = 0.
+Proof.
+remember 0 as n eqn: foo at 1.
+rewrite foo.
+reflexivity.
+Qed.
+
+Goal True.
+Proof.
+assert (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+assert (exists n, n = 0) as [n Hn].
++ exists 0; reflexivity.
++ exact I.
+Qed.
+
+Goal True -> True.
+Proof.
+assert (H : 0 + 0 = 0) by reflexivity.
+intros x; exact x.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+change (?a + 1 = 2) with (2 = $a + 1).
+reflexivity.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl).
+destruct H.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl) as [].
+Qed.
diff --git a/test-suite/ltac2/matching.v b/test-suite/ltac2/matching.v
new file mode 100644
index 0000000000..4338cbd32f
--- /dev/null
+++ b/test-suite/ltac2/matching.v
@@ -0,0 +1,71 @@
+Require Import Ltac2.Ltac2 Ltac2.Notations.
+
+Ltac2 Type exn ::= [ Nope ].
+
+Ltac2 check_id id id' := match Ident.equal id id' with
+| true => ()
+| false => Control.throw Nope
+end.
+
+Goal True -> False.
+Proof.
+Fail
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => Message.print (Message.of_constr c); b.(contents) := false; fail
+  | false => ()
+  end
+in
+(** This fails because the matching is not allowed to backtrack once
+    it commits to a branch*)
+lazy_match! '(nat -> bool) with context [?a] => f a end.
+lazy_match! Control.goal () with ?a -> ?b => Message.print (Message.of_constr b) end.
+
+(** This one works by taking the second match context, i.e. ?a := nat *)
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => b.(contents) := false; fail
+  | false => Message.print (Message.of_constr c)
+  end
+in
+match! '(nat -> bool) with context [?a] => f a end.
+Abort.
+
+Goal forall (i j : unit) (x y : nat) (b : bool), True.
+Proof.
+Fail match! goal with
+| [ h : ?t, h' : ?t |- _ ] => ()
+end.
+intros i j x y b.
+match! goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @x;
+  check_id h' @y
+end.
+match! reverse goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @j;
+  check_id h' @i
+end.
+Abort.
+
+(* Check #79 *)
+Goal 2 = 3.
+  Control.plus
+    (fun ()
+     => lazy_match! goal with
+    | [ |- 2 = 3 ] => Control.zero (Tactic_failure None)
+    | [ |- 2 = _ ] => Control.zero (Tactic_failure (Some (Message.of_string "should not be printed")))
+     end)
+    (fun e
+     => match e with
+        | Tactic_failure c
+          => match c with
+             | None => ()
+             | _ => Control.zero e
+             end
+        | e => Control.zero e
+        end).
+Abort.
diff --git a/test-suite/ltac2/quot.v b/test-suite/ltac2/quot.v
new file mode 100644
index 0000000000..624c4ad0c1
--- /dev/null
+++ b/test-suite/ltac2/quot.v
@@ -0,0 +1,26 @@
+Require Import Ltac2.Ltac2.
+
+(** Test for quotations *)
+
+Ltac2 ref0 () := reference:(&x).
+Ltac2 ref1 () := reference:(nat).
+Ltac2 ref2 () := reference:(Datatypes.nat).
+Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
+Fail Ltac2 ref () := reference:(And.Me.neither).
+
+Goal True.
+Proof.
+let x := constr:(I) in
+let y := constr:((fun z => z) $x) in
+Control.refine (fun _ => y).
+Qed.
+
+Goal True.
+Proof.
+(** Here, Ltac2 should not put its variables in the same environment as
+    Ltac1 otherwise the second binding fails as x is bound but not an
+    ident. *)
+let x := constr:(I) in
+let y := constr:((fun x => x) $x) in
+Control.refine (fun _ => y).
+Qed.
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
new file mode 100644
index 0000000000..e1c20a2059
--- /dev/null
+++ b/test-suite/ltac2/rebind.v
@@ -0,0 +1,34 @@
+Require Import Ltac2.Ltac2 Ltac2.Notations.
+
+Ltac2 mutable foo () := constructor.
+
+Goal True.
+Proof.
+foo ().
+Qed.
+
+Ltac2 Set foo := fun _ => fail.
+
+Goal True.
+Proof.
+Fail foo ().
+constructor.
+Qed.
+
+(** Not the right type *)
+Fail Ltac2 Set foo := 0.
+
+Ltac2 bar () := ().
+
+(** Cannot redefine non-mutable tactics *)
+Fail Ltac2 Set bar := fun _ => ().
+
+(** Subtype check *)
+
+Ltac2 mutable rec f x := f x.
+
+Fail Ltac2 Set f := fun x => x.
+
+Ltac2 mutable g x := x.
+
+Ltac2 Set g := f.
diff --git a/test-suite/ltac2/stuff/ltac2.v b/test-suite/ltac2/stuff/ltac2.v
new file mode 100644
index 0000000000..370bc70d15
--- /dev/null
+++ b/test-suite/ltac2/stuff/ltac2.v
@@ -0,0 +1,143 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 foo (_ : int) :=
+  let f (x : int) := x in
+  let _ := f 0 in
+  f 1.
+
+Print Ltac2 foo.
+
+Import Control.
+
+Ltac2 exact x := refine (fun () => x).
+
+Print Ltac2 refine.
+Print Ltac2 exact.
+
+Ltac2 foo' () := ident:(bla).
+
+Print Ltac2 foo'.
+
+Ltac2 bar x h := match x with
+| None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat)
+| Some x => x
+end.
+
+Print Ltac2 bar.
+
+Ltac2 qux := Some 0.
+
+Print Ltac2 qux.
+
+Ltac2 Type foo := [ Foo (int) ].
+
+Fail Ltac2 qux0 := Foo None.
+
+Ltac2 Type 'a ref := { mutable contents : 'a }.
+
+Fail Ltac2 qux0 := { contents := None }.
+Ltac2 foo0 () := { contents := None }.
+
+Print Ltac2 foo0.
+
+Ltac2 qux0 x := x.(contents).
+Ltac2 qux1 x := x.(contents) := x.(contents).
+
+Ltac2 qux2 := ([1;2], true).
+
+Print Ltac2 qux0.
+Print Ltac2 qux1.
+Print Ltac2 qux2.
+
+Import Control.
+
+Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))).
+
+Print Ltac2 qux3.
+
+Ltac2 Type rec nat := [ O | S (nat) ].
+
+Ltac2 message_of_nat n :=
+let rec aux n :=
+match n with
+| O => Message.of_string "O"
+| S n => Message.concat (Message.of_string "S") (aux n)
+end in aux n.
+
+Print Ltac2 message_of_nat.
+
+Ltac2 numgoals () :=
+  let r := { contents := O } in
+  enter (fun () => r.(contents) := S (r.(contents)));
+  r.(contents).
+
+Print Ltac2 numgoals.
+
+Goal True /\ False.
+Proof.
+let n := numgoals () in Message.print (message_of_nat n).
+refine (fun () => open_constr:((fun x => conj _ _) 0)); ().
+let n := numgoals () in Message.print (message_of_nat n).
+
+Fail (hyp ident:(x)).
+Fail (enter (fun () => hyp ident:(There_is_no_spoon); ())).
+
+enter (fun () => Message.print (Message.of_string "foo")).
+
+enter (fun () => Message.print (Message.of_constr (goal ()))).
+Fail enter (fun () => Message.print (Message.of_constr (qux3 ident:(x)))).
+enter (fun () => plus (fun () => constr:(_); ()) (fun _ => ())).
+plus
+  (fun () => enter (fun () => let x := ident:(foo) in let _ := hyp x in ())) (fun _ => Message.print (Message.of_string "failed")).
+let x := { contents := 0 } in
+let x := x.(contents) := x.(contents) in x.
+Abort.
+
+Ltac2 Type exn ::= [ Foo ].
+
+Goal True.
+Proof.
+plus (fun () => zero Foo) (fun _ => ()).
+Abort.
+
+Ltac2 Type exn ::= [ Bar (string) ].
+
+Goal True.
+Proof.
+Fail zero (Bar "lol").
+Abort.
+
+Ltac2 Notation "refine!" c(thunk(constr)) := refine c.
+
+Goal True.
+Proof.
+refine! I.
+Abort.
+
+Goal True.
+Proof.
+let x () := plus (fun () => 0) (fun _ => 1) in
+match case x with
+| Val x =>
+  match x with
+  | (x, k) => Message.print (Message.of_int (k Not_found))
+  end
+| Err x => Message.print (Message.of_string "Err")
+end.
+Abort.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+refine (fun () => '(fun H => _)).
+Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
+refine (fun () => 'eq_refl).
+Qed.
+
+Goal forall x, 1 + x = x + 1.
+Proof.
+refine (fun () => '(fun x => _)).
+Std.cbv {
+  Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
+  Std.rZeta := true; Std.rDelta := true; Std.rConst := [];
+} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
+Abort.
diff --git a/test-suite/ltac2/tacticals.v b/test-suite/ltac2/tacticals.v
new file mode 100644
index 0000000000..1a2fbcbb37
--- /dev/null
+++ b/test-suite/ltac2/tacticals.v
@@ -0,0 +1,34 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Goal True.
+Proof.
+Fail fail.
+Fail solve [ () ].
+try fail.
+repeat fail.
+repeat ().
+solve [ constructor ].
+Qed.
+
+Goal True.
+Proof.
+first [
+  Message.print (Message.of_string "Yay"); fail
+| constructor
+| Message.print (Message.of_string "I won't be printed")
+].
+Qed.
+
+Goal True /\ True.
+Proof.
+Fail split > [ split | |].
+split > [split | split].
+Qed.
+
+Goal True /\ (True -> True) /\ True.
+Proof.
+split > [ | split] > [split | .. | split].
+intros H; refine &H.
+Qed.
diff --git a/test-suite/ltac2/typing.v b/test-suite/ltac2/typing.v
new file mode 100644
index 0000000000..9f18292716
--- /dev/null
+++ b/test-suite/ltac2/typing.v
@@ -0,0 +1,72 @@
+Require Import Ltac2.Ltac2.
+
+(** Ltac2 is typed à la ML. *)
+
+Ltac2 test0 n := Int.add n 1.
+
+Print Ltac2 test0.
+
+Ltac2 test1 () := test0 0.
+
+Print Ltac2 test1.
+
+Fail Ltac2 test2 () := test0 true.
+
+Fail Ltac2 test2 () := test0 0 0.
+
+Ltac2 test3 f x := x, (f x, x).
+
+Print Ltac2 test3.
+
+(** Polymorphism *)
+
+Ltac2 rec list_length l :=
+match l with
+| [] => 0
+| x :: l => Int.add 1 (list_length l)
+end.
+
+Print Ltac2 list_length.
+
+(** Pattern-matching *)
+
+Ltac2 ifb b f g := match b with
+| true => f ()
+| false => g ()
+end.
+
+Print Ltac2 ifb.
+
+Ltac2 if_not_found e f g := match e with
+| Not_found => f ()
+| _ => g ()
+end.
+
+Fail Ltac2 ifb' b f g := match b with
+| true => f ()
+end.
+
+Fail Ltac2 if_not_found' e f g := match e with
+| Not_found => f ()
+end.
+
+(** Reimplementing 'do'. Return value of the function useless. *)
+
+Ltac2 rec do n tac := match Int.equal n 0 with
+| true => ()
+| false => tac (); do (Int.sub n 1) tac
+end.
+
+Print Ltac2 do.
+
+(** Non-function pure values are OK. *)
+
+Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")).
+
+Print Ltac2 tuple0.
+
+(** Impure values are not. *)
+
+Fail Ltac2 not_a_value := { contents := 0 }.
+Fail Ltac2 not_a_value := "nope".
+Fail Ltac2 not_a_value := list_length [].
-- 
cgit v1.2.3


From 1ec731fbef3ac13b7a8783461b8fa6609f962054 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 3 May 2019 09:57:06 +0000
Subject: [Test-suite] Add output case for issue #9370

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

(limited to 'test-suite')

diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out
new file mode 100644
index 0000000000..0ff151c8b4
--- /dev/null
+++ b/test-suite/output/bug_9370.out
@@ -0,0 +1,12 @@
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v
new file mode 100644
index 0000000000..a7f4b7c23e
--- /dev/null
+++ b/test-suite/output/bug_9370.v
@@ -0,0 +1,12 @@
+Require Import Reals.
+Open Scope R_scope.
+Goal 1/1=1.
+Proof.
+  field_simplify (1/1).
+Show.
+  field_simplify.
+Show.
+  field_simplify.
+Show.
+  reflexivity.
+Qed.
-- 
cgit v1.2.3


From 21e5a5d510de59a33f3e6a0f88b8321ac0d7d23d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 7 May 2019 12:04:34 -0700
Subject: Show diffs in error messages only if Diffs is enabled

---
 test-suite/output/Error_msg_diffs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
index 11c766b210..a26e683398 100644
--- a/test-suite/output/Error_msg_diffs.v
+++ b/test-suite/output/Error_msg_diffs.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* coq-prog-args: ("-color" "on" "-diffs" "on" "-async-proofs" "off") *)
 (* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
 (* Shows diffs in an error message for an "Unable to unify" error *)
 Require Import Arith List Bool.
-- 
cgit v1.2.3


From 963b950f201614078a432d1ac7568e8757d8df19 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 8 May 2019 20:51:31 +0200
Subject: Add a test that unreleased changelog of released versions is empty.

This test is active only when configure `is_a_released_version` is set
to true. In this case, to pass the test-suite, there must be no
unreleased changelog entries left, i.e. `doc/changelog/*/` must only
contain `00000-title.rst` files.
---
 test-suite/dune              |  2 ++
 test-suite/misc/changelog.sh | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100755 test-suite/misc/changelog.sh

(limited to 'test-suite')

diff --git a/test-suite/dune b/test-suite/dune
index c430400ba5..cd33319fa4 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -20,6 +20,8 @@
    ../dev/header.ml
    ../dev/tools/update-compat.py
    ../doc/stdlib/index-list.html.template
+   ; For the changelog test
+   ../config/coq_config.py
    (package coq)
    ; For fake_ide
    (package coqide-server)
diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh
new file mode 100755
index 0000000000..8b4a49e577
--- /dev/null
+++ b/test-suite/misc/changelog.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+while read line; do
+  if [ "$line" = "is_a_released_version = False" ]; then
+    echo "This is not a released version: nothing to test."
+    exit 0
+  fi
+done < ../config/coq_config.py
+
+for d in ../doc/changelog/*; do
+  if [ -d "$d" ]; then
+    if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then
+      echo "Fatal: unreleased changelog entries remain in ${d#../}/"
+      echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/"
+      exit 1
+    fi
+  fi
+done
-- 
cgit v1.2.3


From 857082b492760c17bfbc2b2022862c7cd758261e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 2 May 2019 21:28:47 +0200
Subject: Remove various circumvolutions from reduction behaviors

Incidentally, this fixes #10056
---
 test-suite/output/Arguments.out          | 24 +++++++++++++++++-------
 test-suite/output/Arguments.v            |  9 +++++++++
 test-suite/output/Arguments_renaming.out |  4 ++--
 3 files changed, 28 insertions(+), 9 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 7074ad2d41..3c1e27ba9d 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -27,7 +27,7 @@ Nat.sub : nat -> nat -> nat
 Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor and when applied to 2 arguments 
+  2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
@@ -35,7 +35,7 @@ Nat.sub : nat -> nat -> nat
 Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor 
+  2nd arguments evaluate to a constructor
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 pf :
@@ -54,7 +54,7 @@ fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 fcomp is not universe polymorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
-The reduction tactics unfold fcomp when applied to 6 arguments 
+The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
@@ -75,7 +75,7 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat
 f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
-  5th arguments evaluate to a constructor 
+  5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
@@ -84,7 +84,7 @@ f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
-  6th arguments evaluate to a constructor 
+  6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
@@ -93,7 +93,7 @@ f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor 
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
      = forall v : unit, f 0 0 5 v 3 = 2
@@ -104,7 +104,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor 
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
 forall w : r, w 3 true = tt
@@ -115,3 +115,13 @@ w 3 true = tt
      : Prop
 The command has indeed failed with message:
 Extra arguments: _, _.
+volatilematch : nat -> nat
+
+volatilematch is not universe polymorphic
+Argument scope is [nat_scope]
+The reduction tactics always unfold volatilematch
+  but avoid exposing match constructs
+volatilematch is transparent
+Expands to: Constant Arguments.volatilematch
+     = fun n : nat => volatilematch n
+     : nat -> nat
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 844f96aaa1..b909f1b64c 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -55,3 +55,12 @@ Arguments w  x%F y%B : extra scopes.
 Check (w $ $ = tt).
 Fail Arguments w  _%F _%B.
 
+Definition volatilematch (n : nat) :=
+  match n with
+  | O => O
+  | S p => p
+  end.
+
+Arguments volatilematch / n : simpl nomatch.
+About volatilematch.
+Eval simpl in fun n => volatilematch n.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3f0717666c..65c902202d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -62,7 +62,7 @@ Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor 
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
@@ -101,7 +101,7 @@ Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor 
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.myplus
 @myplus
-- 
cgit v1.2.3


From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 9 May 2019 13:39:25 +0000
Subject: [Attributes] Allow explicit value for two-valued attributes

Attributes that enable/disable a feature can have an explicit value
(default is enable when the attribute is present).

Three-valued boolean attributes do not support this:
what would `#[local(false)]` mean?
---
 test-suite/success/attribute_syntax.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index f4f59a3c16..4717759dec 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -20,6 +20,10 @@ Check ι _ ι.
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
 
-- 
cgit v1.2.3


From beb5bdec79ff371f48a478df3c24f2cf9d68aa1f Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 7 May 2019 15:04:04 -0700
Subject: Use Print Custom Grammar to inspect custom entries

---
 test-suite/output/Notations4.out | 10 ++++++++++
 test-suite/output/Notations4.v   |  1 +
 test-suite/success/Notations2.v  |  4 ++--
 3 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 9d972a68f7..c1b9a2b1c6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,15 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+Entry constr:myconstr is
+[ "6" RIGHTA
+  [  ]
+| "5" RIGHTA
+  [ SELF;  "+"; NEXT ]
+| "4" RIGHTA
+  [ SELF;  "*"; NEXT ]
+| "3" RIGHTA
+  [  "<"; constr:operconstr LEVEL "10";  ">" ] ]
+
 [< b > + < b > * < 2 >]
      : nat
 [<< # 0 >>]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 81c64418cb..d1063bfd04 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
 Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
+Print Custom Grammar myconstr.
 
 Axiom a : nat.
 Notation b := a.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 2533a39cc4..d047f7560e 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -151,8 +151,8 @@ Module M16.
   Local Notation "##" := 0 (in custom foo2).
 
   (* Test Print Grammar *)
-  Print Grammar foo.
-  Print Grammar foo2.
+  Print Custom Grammar foo.
+  Print Custom Grammar foo2.
 End M16.
 
 (* Example showing the need for strong evaluation of
-- 
cgit v1.2.3


From cf9f4e566b87d2875f757bb7d54ee4421988e315 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 10 May 2019 12:32:07 +0200
Subject: Make detyping robust w.r.t. indexed anonymous variables

I don't think there's a reason to treat such variables more severely
than unbound variables. This anomaly is often raised by debug printers
(e.g. when studying complex scenarios using `Set Unification Debug`),
and so makes debugging less convenient.

Fixes #3754, fixes #10026.
---
 test-suite/bugs/closed/bug_10026.v |   3 +
 test-suite/bugs/closed/bug_3754.v  | 287 +++++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/bug_3754.v  | 285 ------------------------------------
 3 files changed, 290 insertions(+), 285 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_10026.v
 create mode 100644 test-suite/bugs/closed/bug_3754.v
 delete mode 100644 test-suite/bugs/opened/bug_3754.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v
new file mode 100644
index 0000000000..0d3142d0f2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10026.v
@@ -0,0 +1,3 @@
+Require Import Coq.Lists.List.
+Set Debug RAKAM.
+Check fun _ => fold_right (fun A B => prod A B) unit _.
diff --git a/test-suite/bugs/closed/bug_3754.v b/test-suite/bugs/closed/bug_3754.v
new file mode 100644
index 0000000000..7031cbf132
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3754.v
@@ -0,0 +1,287 @@
+Unset Strict Universe Declaration.
+Require Import TestSuite.admit.
+(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
+   coqtop version trunk (October 2014) *)
+
+Notation Type0 := Set.
+
+Notation idmap := (fun x => x).
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+
+Notation pr1 := projT1.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) :=
+  fun x => g (f x).
+
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x.
+admit.
+Defined.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope.
+
+Notation "p @' q" := (concat p q) (at level 21, left associativity,
+  format "'[v' p '/' '@''  q ']'") : long_path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y.
+exact (match p with idpath => u end).
+Defined.
+
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y.
+exact (match p with idpath => idpath end).
+Defined.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B} f {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Local Open Scope trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+Notation IsHProp := (IsTrunc -1).
+
+Monomorphic Axiom dummy_funext_type : Type0.
+Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
+
+Local Open Scope path_scope.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  p @ (q @ r) = (p @ q) @ r :=
+  match r with idpath =>
+    match q with idpath =>
+      match p with idpath => 1
+      end end end.
+
+Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  (p @ q) @ r = p @ (q @ r) :=
+  match r with idpath =>
+    match q with idpath =>
+      match p with idpath => 1
+      end end end.
+
+Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
+  r^ @ q = p -> q = r @ p.
+admit.
+Defined.
+
+Ltac with_rassoc tac :=
+  repeat rewrite concat_pp_p;
+  tac;
+
+  repeat rewrite concat_p_pp.
+
+Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp).
+
+Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A}
+  (r : w = f x) (p : x = y) (q : y = z) :
+  r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q).
+admit.
+Defined.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ (ap g q)
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type)
+  {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z)
+  : D x2 (p # y) (p # z)
+  :=
+  match p with idpath => w end.
+Local Open Scope equiv_scope.
+
+Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2)
+  : (transport (fun x => B x -> C) p f) y  =  f (p^ # y).
+admit.
+Defined.
+
+Definition transport_arrow_fromconst {A B : Type} {C : A -> Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B)
+  : (transport (fun x => B -> C x) p f) y  =  p # (f y).
+admit.
+Defined.
+
+Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2)
+  : ap (transport (fun x => B x -> C) p f) q
+    @ transport_arrow_toconst p f y2
+    = transport_arrow_toconst p f y1
+    @ ap (fun y => f (p^ # y)) q.
+admit.
+Defined.
+
+Class Univalence.
+Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B).
+admit.
+Defined.
+Definition transport_path_universe
+           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
+  : transport (fun X:Type => X) (path_universe f) z = f z.
+admit.
+Defined.
+Definition transport_path_universe_V `{Funext}
+           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B)
+  : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z.
+admit.
+Defined.
+
+Ltac simpl_do_clear tac term :=
+  let H := fresh in
+  assert (H := term);
+    simpl in H |- *;
+    tac H;
+    clear H.
+
+Tactic Notation "simpl" "rewrite"      constr(term) := simpl_do_clear ltac:(fun H => rewrite    H) term.
+
+Global Instance Univalence_implies_Funext `{Univalence} : Funext.
+Admitted.
+
+Section Factorization.
+
+  Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}}
+          `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)}
+          `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)}
+          {A B : Type@{i}} {f : A -> B}.
+
+  Record Factorization :=
+    { intermediate : Type ;
+      factor1 : A -> intermediate ;
+      factor2 : intermediate -> B ;
+      fact_factors : factor2 o factor1 == f ;
+      inclass1 : class1 _ _ factor1 ;
+      inclass2 : class2 _ _ factor2
+    }.
+
+  Record PathFactorization {fact fact' : Factorization} :=
+    { path_intermediate : intermediate fact <~> intermediate fact' ;
+      path_factor1 : path_intermediate o factor1 fact == factor1 fact' ;
+      path_factor2 : factor2 fact == factor2 fact' o path_intermediate ;
+      path_fact_factors : forall a, path_factor2 (factor1 fact a)
+                          @ ap (factor2 fact') (path_factor1 a)
+                          @ fact_factors fact' a
+                          = fact_factors fact a
+    }.
+    Context `{Univalence} {fact fact' : Factorization}
+            (pf : @PathFactorization fact fact').
+
+    Let II := path_intermediate pf.
+    Let ff1 := path_factor1 pf.
+    Let ff2 := path_factor2 pf.
+Local Definition II' : intermediate fact = intermediate fact'.
+admit.
+Defined.
+
+    Local Definition fff' (a : A)
+    : (transportD2 (fun X => A -> X) (fun X => X -> B)
+                   (fun X g h => {_ : forall a : A, h (g a) = f a &
+                                  {_ : class1 A X g & class2 X B h}})
+                   II' (factor1 fact) (factor2 fact)
+                   (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a =
+      ap (transport (fun X => X -> B) II' (factor2 fact))
+        (transport_arrow_fromconst II' (factor1 fact) a
+          @ transport_path_universe II (factor1 fact a)
+          @ ff1 a)
+        @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a)
+        @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a))
+        @ ff2 (II^-1 (factor1 fact' a))
+        @ ap (factor2 fact') (eisretr II (factor1 fact' a))
+        @ fact_factors fact' a.
+    Proof.
+
+      Open Scope long_path_scope.
+
+      rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)).
+
+      simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^)
+                                 (factor2 fact)).
+      rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
+      Set Debug Tactic Unification.
+      rewrite (concat_Ap ff2).
+    Abort.
+
+End Factorization.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v
deleted file mode 100644
index 18820b1a4c..0000000000
--- a/test-suite/bugs/opened/bug_3754.v
+++ /dev/null
@@ -1,285 +0,0 @@
-Unset Strict Universe Declaration.
-Require Import TestSuite.admit.
-(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
-(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
-   coqtop version trunk (October 2014) *)
-
-Notation Type0 := Set.
-
-Notation idmap := (fun x => x).
-
-Notation "( x ; y )" := (existT _ x y) : fibration_scope.
-Open Scope fibration_scope.
-
-Notation pr1 := projT1.
-
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) :=
-  fun x => g (f x).
-
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Arguments idpath {A a} , [A] a.
-
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-Definition inverse {A : Type} {x y : A} (p : x = y) : y = x.
-admit.
-Defined.
-
-Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
-  match p, q with idpath, idpath => idpath end.
-
-Notation "1" := idpath : path_scope.
-
-Notation "p @ q" := (concat p q) (at level 20) : path_scope.
-
-Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope.
-
-Notation "p @' q" := (concat p q) (at level 21, left associativity,
-  format "'[v' p '/' '@''  q ']'") : long_path_scope.
-Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y.
-exact (match p with idpath => u end).
-Defined.
-
-Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y.
-exact (match p with idpath => idpath end).
-Defined.
-
-Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
-  := forall x:A, f x = g x.
-
-Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
-
-Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
-  forall x : A, r (s x) = x.
-
-Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
-  equiv_inv : B -> A ;
-  eisretr : Sect equiv_inv f;
-  eissect : Sect f equiv_inv;
-  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
-}.
-
-Arguments eisretr {A B} f {_} _.
-
-Record Equiv A B := BuildEquiv {
-  equiv_fun : A -> B ;
-  equiv_isequiv : IsEquiv equiv_fun
-}.
-
-Coercion equiv_fun : Equiv >-> Funclass.
-
-Global Existing Instance equiv_isequiv.
-
-Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
-
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-
-Class Contr_internal (A : Type) := BuildContr {
-  center : A ;
-  contr : (forall y : A, center = y)
-}.
-
-Inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index -> trunc_index.
-
-Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
-Local Open Scope trunc_scope.
-Notation "-2" := minus_two (at level 0) : trunc_scope.
-Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
-
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
-  match n with
-    | -2 => Contr_internal A
-    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
-  end.
-
-Class IsTrunc (n : trunc_index) (A : Type) : Type :=
-  Trunc_is_trunc : IsTrunc_internal n A.
-Notation IsHProp := (IsTrunc -1).
-
-Monomorphic Axiom dummy_funext_type : Type0.
-Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
-
-Local Open Scope path_scope.
-
-Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
-  p @ 1 = p
-  :=
-  match p with idpath => 1 end.
-
-Definition concat_1p {A : Type} {x y : A} (p : x = y) :
-  1 @ p = p
-  :=
-  match p with idpath => 1 end.
-
-Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
-  p @ (q @ r) = (p @ q) @ r :=
-  match r with idpath =>
-    match q with idpath =>
-      match p with idpath => 1
-      end end end.
-
-Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
-  (p @ q) @ r = p @ (q @ r) :=
-  match r with idpath =>
-    match q with idpath =>
-      match p with idpath => 1
-      end end end.
-
-Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
-  r^ @ q = p -> q = r @ p.
-admit.
-Defined.
-
-Ltac with_rassoc tac :=
-  repeat rewrite concat_pp_p;
-  tac;
-
-  repeat rewrite concat_p_pp.
-
-Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp).
-
-Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A}
-  (r : w = f x) (p : x = y) (q : y = z) :
-  r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q).
-admit.
-Defined.
-
-Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
-  ap (g o f) p = ap g (ap f p)
-  :=
-  match p with idpath => 1 end.
-
-Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
-  (ap f q) @ (p y) = (p x) @ (ap g q)
-  :=
-  match q with
-    | idpath => concat_1p _ @ ((concat_p1 _) ^)
-  end.
-
-Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type)
-  {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z)
-  : D x2 (p # y) (p # z)
-  :=
-  match p with idpath => w end.
-Local Open Scope equiv_scope.
-
-Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
-  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2)
-  : (transport (fun x => B x -> C) p f) y  =  f (p^ # y).
-admit.
-Defined.
-
-Definition transport_arrow_fromconst {A B : Type} {C : A -> Type}
-  {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B)
-  : (transport (fun x => B -> C x) p f) y  =  p # (f y).
-admit.
-Defined.
-
-Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
-  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2)
-  : ap (transport (fun x => B x -> C) p f) q
-    @ transport_arrow_toconst p f y2
-    = transport_arrow_toconst p f y1
-    @ ap (fun y => f (p^ # y)) q.
-admit.
-Defined.
-
-Class Univalence.
-Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B).
-admit.
-Defined.
-Definition transport_path_universe
-           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
-  : transport (fun X:Type => X) (path_universe f) z = f z.
-admit.
-Defined.
-Definition transport_path_universe_V `{Funext}
-           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B)
-  : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z.
-admit.
-Defined.
-
-Ltac simpl_do_clear tac term :=
-  let H := fresh in
-  assert (H := term);
-    simpl in H |- *;
-    tac H;
-    clear H.
-
-Tactic Notation "simpl" "rewrite"      constr(term) := simpl_do_clear ltac:(fun H => rewrite    H) term.
-
-Global Instance Univalence_implies_Funext `{Univalence} : Funext.
-Admitted.
-
-Section Factorization.
-
-  Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}}
-          `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)}
-          `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)}
-          {A B : Type@{i}} {f : A -> B}.
-
-  Record Factorization :=
-    { intermediate : Type ;
-      factor1 : A -> intermediate ;
-      factor2 : intermediate -> B ;
-      fact_factors : factor2 o factor1 == f ;
-      inclass1 : class1 _ _ factor1 ;
-      inclass2 : class2 _ _ factor2
-    }.
-
-  Record PathFactorization {fact fact' : Factorization} :=
-    { path_intermediate : intermediate fact <~> intermediate fact' ;
-      path_factor1 : path_intermediate o factor1 fact == factor1 fact' ;
-      path_factor2 : factor2 fact == factor2 fact' o path_intermediate ;
-      path_fact_factors : forall a, path_factor2 (factor1 fact a)
-                          @ ap (factor2 fact') (path_factor1 a)
-                          @ fact_factors fact' a
-                          = fact_factors fact a
-    }.
-    Context `{Univalence} {fact fact' : Factorization}
-            (pf : @PathFactorization fact fact').
-
-    Let II := path_intermediate pf.
-    Let ff1 := path_factor1 pf.
-    Let ff2 := path_factor2 pf.
-Local Definition II' : intermediate fact = intermediate fact'.
-admit.
-Defined.
-
-    Local Definition fff' (a : A)
-    : (transportD2 (fun X => A -> X) (fun X => X -> B)
-                   (fun X g h => {_ : forall a : A, h (g a) = f a &
-                                  {_ : class1 A X g & class2 X B h}})
-                   II' (factor1 fact) (factor2 fact)
-                   (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a =
-      ap (transport (fun X => X -> B) II' (factor2 fact))
-        (transport_arrow_fromconst II' (factor1 fact) a
-          @ transport_path_universe II (factor1 fact a)
-          @ ff1 a)
-        @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a)
-        @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a))
-        @ ff2 (II^-1 (factor1 fact' a))
-        @ ap (factor2 fact') (eisretr II (factor1 fact' a))
-        @ fact_factors fact' a.
-    Proof.
-
-      Open Scope long_path_scope.
-
-      rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)).
-
-      simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^)
-                                 (factor2 fact)).
-      rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
-      Set Debug Tactic Unification.
-      Fail rewrite (concat_Ap ff2).
-    Abort.
-- 
cgit v1.2.3


From d8d665f900ee92fac8f776031a9a6a0981a4ed2e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sun, 19 May 2019 01:38:59 -0700
Subject: Implicit Quantifiers recurse in continuation of let-in

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v
new file mode 100644
index 0000000000..d603bff386
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10189.v
@@ -0,0 +1,9 @@
+Definition foo : forall (x := unit) {y : nat}, nat := fun y => y.
+Check foo (y := 3). (*We fail to get implicits in the type past a let-in*)
+Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y.
+Check foo' unit (y := 3). (* It works with a function binder *)
+
+Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3).
+(* Adding bar : nat -> nat gives implicits-in-term warning *)
+Fail Check bar (x := 3).
+(* The implicits from the type of the local definition leak to the outer term *)
-- 
cgit v1.2.3


From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:06:32 +0100
Subject: Remove Refine Instance Mode option

---
 test-suite/success/Typeclasses.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3888cafed3..736d05fefc 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,9 +198,7 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
-    Set Refine Instance Mode.
-    Instance eqa : Eq nat := _. constructor. Qed.
-    Unset Refine Instance Mode.
+    Instance eqa : Eq nat. Qed.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
-- 
cgit v1.2.3


From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:48:36 +0100
Subject: Remove VtUnknown classification

This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.

The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.

We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.

Fixes #3632 #3890 #4638.
---
 test-suite/bugs/closed/bug_3890.v | 12 ++++++++++++
 test-suite/bugs/closed/bug_4580.v |  1 -
 test-suite/bugs/closed/bug_4638.v | 12 ++++++++++++
 test-suite/bugs/opened/bug_3890.v | 22 ----------------------
 4 files changed, 24 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_3890.v
 create mode 100644 test-suite/bugs/closed/bug_4638.v
 delete mode 100644 test-suite/bugs/opened/bug_3890.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
 
 Class Foo (A : Type) := foo : A.
 
-Unset Refine Instance Mode.
 Program Instance f1 : Foo nat := S _.
 Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
deleted file mode 100644
index 9d83743b2a..0000000000
--- a/test-suite/bugs/opened/bug_3890.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Nested Proofs Allowed.
-
-Class Foo.
-Class Bar := b : Type.
-
-Set Refine Instance Mode.
-Instance foo : Foo := _.
-Unset Refine Instance Mode.
-(* 1 subgoals, subgoal 1 (ID 4)
-
-  ============================
-   Foo *)
-
-Instance bar : Bar.
-exact Type.
-Defined.
-(* bar is defined *)
-
-About foo.
-(* foo not a defined object. *)
-
-Fail Defined.
-- 
cgit v1.2.3