From 265be83a546b0bec6d01f6650f7489442293cb0e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 May 2016 18:02:08 +0200
Subject: Hints/Univs: fix bug #4628 anomalies

Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).
---
 test-suite/bugs/closed/4628.v | 46 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 test-suite/bugs/closed/4628.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v
new file mode 100644
index 0000000000..7d4a15d689
--- /dev/null
+++ b/test-suite/bugs/closed/4628.v
@@ -0,0 +1,46 @@
+Module first.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End first.
+
+Module firstbest.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Polymorphic Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End firstbest.
+
+Module second.
+Axiom foo: Set.
+Axiom foo': Set.
+
+Polymorphic Record BAR (A:Type) :=
+  { bar: foo' -> foo}.
+Set Printing Universes.
+
+Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
+  eauto using bar.
+Qed.
+End second.
-- 
cgit v1.2.3


From 891a8a9f7ea3bb5b0b07dc5a2df51314135d8b53 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 May 2016 18:58:01 +0200
Subject: Extraction/Projections: Fix bug #4710

Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
---
 test-suite/bugs/closed/4710.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/closed/4710.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
new file mode 100644
index 0000000000..fdc8501099
--- /dev/null
+++ b/test-suite/bugs/closed/4710.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : nat }.
+Extraction foo.
+Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
+Extraction Language Ocaml.
+Extraction foo2p.
+
+Definition bla (x : Foo2 0) := foo2p _ x.
+Extraction bla.
+
+Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
+Extraction bla'.
-- 
cgit v1.2.3


From 9de5a59aa6994e8023b9e551b232a73aab3521fa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 May 2016 11:32:51 +0200
Subject: rewrite/Univs: Fix bug # 4498.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
new file mode 100644
index 0000000000..ccdb2dddda
--- /dev/null
+++ b/test-suite/bugs/closed/4498.v
@@ -0,0 +1,24 @@
+Require Export Coq.Unicode.Utf8.
+Require Export Coq.Classes.Morphisms.
+Require Export Coq.Relations.Relation_Definitions.
+
+Set Universe Polymorphism.
+
+Reserved Notation "a ~> b" (at level 90, right associativity).
+
+Class Category := {
+  ob            : Type;
+  uhom          := Type : Type;
+  hom           : ob → ob → uhom where "a ~> b" := (hom a b);
+  compose       : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C);
+  equiv         : ∀ {A B}, relation (A ~> B);
+  is_equiv      : ∀ {A B}, @Equivalence (A ~> B) equiv;
+  comp_respects : ∀ {A B C},
+      Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
+}.
+
+Require Export Coq.Setoids.Setoid.
+
+Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+  signature equiv ==> equiv ==> equiv as compose_mor.
+Proof. apply comp_respects. Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From 35fb7ad402fee1e3e247ccf37438d3a7a5230629 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 May 2016 15:58:21 +0200
Subject: Fix bug #4746: Anomaly: Evar ?X10 was not declared.

Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.

Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
---
 test-suite/bugs/closed/4746.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/4746.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v
new file mode 100644
index 0000000000..d64cc6fe68
--- /dev/null
+++ b/test-suite/bugs/closed/4746.v
@@ -0,0 +1,14 @@
+Variables P Q : nat -> Prop.
+Variable f : nat -> nat.
+
+Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False.
+Proof.
+intros.
+ecase H with (3:=eq_refl).
+Abort.
+
+Goal forall (x:nat), (forall y, y=x -> False) -> False.
+Proof.
+intros.
+unshelve ecase H with (1:=eq_refl).
+Qed.
-- 
cgit v1.2.3