From be4bfc78c493464cb0af40d7fae08ba86295a6f9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 20:49:34 +0100
Subject: Fixing #4256 and #4484 (changes in evar-evar resolution made that new
 evars were created making in turn that evars formerly recognized as pending
 were not anymore in the list of pending evars). This also fixes the reopening
 of #3848.

See comments on #4484 for details.
---
 test-suite/bugs/closed/3848.v | 22 ++++++++++++++++++++++
 test-suite/bugs/closed/4256.v | 43 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/4484.v | 10 ++++++++++
 test-suite/bugs/opened/3848.v | 22 ----------------------
 4 files changed, 75 insertions(+), 22 deletions(-)
 create mode 100644 test-suite/bugs/closed/3848.v
 create mode 100644 test-suite/bugs/closed/4256.v
 create mode 100644 test-suite/bugs/closed/4484.v
 delete mode 100644 test-suite/bugs/opened/3848.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
new file mode 100644
index 0000000000..a03e8ffdab
--- /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)).
+Fail Defined. (* 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/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).
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
deleted file mode 100644
index a03e8ffdab..0000000000
--- a/test-suite/bugs/opened/3848.v
+++ /dev/null
@@ -1,22 +0,0 @@
-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)).
-Fail Defined. (* Error: Attempt to save an incomplete proof *)
-- 
cgit v1.2.3