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

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

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

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

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

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/bugs/closed/bug_10031.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10031.v

(limited to 'test-suite/bugs')

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

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

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

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