From 0b417c12eb10bb29bcee04384b6c0855cb9de73a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 5 Oct 2016 17:50:45 +0200
Subject: unification.ml: fix for bug #4763, unif regression

Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
---
 test-suite/bugs/closed/4763.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/4763.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 0000000000..ae8ed0e6e8
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Coercion is_true : bool >-> Sortclass.
+Global Instance: Transitive leb.
+Admitted.
+
+Goal forall x y z, leb x y -> leb y z -> True.
+  intros ??? H H'.
+  lazymatch goal with
+  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
+    => pose proof (transitivity H H' : is_true (R x z))
+  end.
+  exact I.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From 0a6f0c161756a1878dd81e438df86f08631d8399 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 11:38:06 +0200
Subject: evarconv.ml: Fix bug #4529, primproj unfolding

Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
---
 test-suite/bugs/closed/4529.v | 45 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 test-suite/bugs/closed/4529.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v
new file mode 100644
index 0000000000..8b3c24fec6
--- /dev/null
+++ b/test-suite/bugs/closed/4529.v
@@ -0,0 +1,45 @@
+(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *)
+(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3
+   coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *)
+Require Coq.Setoids.Setoid.
+Import Coq.Setoids.Setoid.
+
+Class Equiv A := equiv: relation A.
+Infix "≡" := equiv (at level 70, no associativity).
+Notation "(≡)" := equiv (only parsing).
+
+(* If I remove this line, everything compiles. *)
+Set Primitive Projections.
+
+Class Dist A := dist : nat -> relation A.
+Notation "x ={ n }= y" := (dist n x y)
+  (at level 70, n at next level, format "x  ={ n }=  y").
+
+Record CofeMixin A `{Equiv A, Dist A} := {
+  mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y;
+  mixin_dist_equivalence n : Equivalence (dist n);
+}.
+
+Structure cofeT := CofeT {
+  cofe_car :> Type;
+  cofe_equiv : Equiv cofe_car;
+  cofe_dist : Dist cofe_car;
+  cofe_mixin : CofeMixin cofe_car
+}.
+Existing Instances cofe_equiv cofe_dist.
+Arguments cofe_car : simpl never.
+
+Section cofe_mixin.
+  Context {A : cofeT}.
+  Implicit Types x y : A.
+  Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y.
+Admitted.
+End cofe_mixin.
+  Context {A : cofeT}.
+  Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
+  Proof.
+    split.
+    *
+ intros x.
+apply equiv_dist.
+
-- 
cgit v1.2.3


From d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Oct 2016 18:06:47 +0200
Subject: Fix bug #4464: "Anomaly: variable H' unbound. Please report.".

We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
---
 test-suite/bugs/closed/4464.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4464.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v
new file mode 100644
index 0000000000..f8e9405d93
--- /dev/null
+++ b/test-suite/bugs/closed/4464.v
@@ -0,0 +1,4 @@
+Goal True -> True.
+Proof.
+  intro H'.
+  let H := H' in destruct H; try destruct H.
-- 
cgit v1.2.3


From 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Oct 2016 01:46:09 +0200
Subject: Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v
new file mode 100644
index 0000000000..eed7f0f3ff
--- /dev/null
+++ b/test-suite/bugs/closed/5066.v
@@ -0,0 +1,7 @@
+Require Import Vector.
+
+Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) :=
+  match v1 with
+  | nil _          => v2
+  | cons _ e n' sv => vector_rev sv (cons A e n2 v2)
+  end.
-- 
cgit v1.2.3