Merge branch 'v8.5'

5 files changed, 102 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
new file mode 100644
index 0000000000..c0ef02f1e8
--- /dev/null
+++ b/test-suite/bugs/closed/3848.v
@@ -0,0 +1,22 @@
+Require Import TestSuite.admit.
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables A B f g e n.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
+           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b).
+  admit.
+Defined.
+
+Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
+      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
+: (forall b : B, Q b) -> forall a : A, P a.
+Proof.
+  refine (functor_forall
+            (f^-1)
+            (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
+Defined. (* was: Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 0000000000..3cdc4ada02
--- /dev/null
+++ b/test-suite/bugs/closed/4256.v
@@ -0,0 +1,43 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Global Set Universe Polymorphism.
+Monomorphic Universe i.
+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.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Notation "-1" := (trunc_S minus_two) (at level 0).
+
+Class IsPointed (A : Type) := point : A.
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+Coercion pointed_type : pType >-> Sortclass.
+Existing Instance ispointed_type.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+
+
+Record ooGroup :=
+  { classifying_space : pType@{i} }.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+  (** This works: *)
+  pose (x0 := point X).
+  pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
+  clear H x0.
+  (** But this doesn't: *)
+  pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 0000000000..6f8631d458
--- /dev/null
+++ b/test-suite/bugs/closed/4467.v
@@ -0,0 +1,15 @@
+(* Fixing missing test for variable shadowing *)
+
+Definition test (x y:bool*bool) :=
+  match x with
+  | (e as e1, (true) as e2)
+  | ((true) as e1, e as e2) =>
+    let '(e, b) := y in
+    e
+  | _ => true
+  end.
+
+Goal test (true,false) (true,true) = true.
+(* used to evaluate to "false = true" in 8.4 *)
+reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v
new file mode 100644
index 0000000000..08a86330f2
--- /dev/null
+++ b/test-suite/bugs/closed/4480.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Definition proj (P Q : Prop) := P.
+
+Lemma foo (P : Prop) : proj P P = P.
+Admitted.
+Lemma trueI : True <-> True.
+Admitted.
+Goal True.
+  Fail setoid_rewrite foo.
+  Fail setoid_rewrite trueI.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 0000000000..f988539d62
--- /dev/null
+++ b/test-suite/bugs/closed/4484.v
@@ -0,0 +1,10 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Class A := {}.
+Axiom foo : forall {ac : A}, bool.
+Lemma bar (ac : A) : True.
+Check (match foo as k return foo = k -> True with
+       | true => _
+       | false => _
+       end eq_refl).