From c8721369d1d3e6572138fa7aab65e54f68459db4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Nov 2014 10:45:34 +0100
Subject: Test fixed by PMP's commits from Oct 21.

---
 test-suite/bugs/closed/3258.v | 35 +++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3258.v | 35 -----------------------------------
 2 files changed, 35 insertions(+), 35 deletions(-)
 create mode 100644 test-suite/bugs/closed/3258.v
 delete mode 100644 test-suite/bugs/opened/3258.v

diff --git a/test-suite/bugs/closed/3258.v b/test-suite/bugs/closed/3258.v
new file mode 100644
index 0000000000..a1390e3025
--- /dev/null
+++ b/test-suite/bugs/closed/3258.v
@@ -0,0 +1,35 @@
+Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Program Coq.Setoids.Setoid.
+
+Global Set Implicit Arguments.
+
+Hint Extern 0 => apply reflexivity : typeclass_instances.
+
+Inductive Comp : Type -> Type :=
+| Pick : forall A, (A -> Prop) -> Comp A.
+
+Axiom computes_to : forall A, Comp A -> A -> Prop.
+
+Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
+
+Global Instance refine_PreOrder A : PreOrder (@refine A).
+Admitted.
+Add Parametric Morphism A
+: (@Pick A)
+    with signature
+    (pointwise_relation _ (flip impl))
+      ==> (@refine A)
+      as refine_flip_impl_Pick.
+  admit.
+Defined.
+Definition remove_forall_eq' A x B (P : A -> B -> Prop) : pointwise_relation _ impl (P x) (fun z => forall y : A, y = x -> P y z).
+  admit.
+Defined.
+Goal forall A B (x : A) (P : _ -> _ -> Prop),
+       refine (Pick (fun n : B => forall y, y = x -> P y n))
+              (Pick (fun n : B => P x n)).
+Proof.
+  intros.
+  setoid_rewrite (@remove_forall_eq' _ _ _ _).
+  Undo.
+  (* This failed with NotConvertible at some time *)
+  setoid_rewrite (@remove_forall_eq' _ _ _).
diff --git a/test-suite/bugs/opened/3258.v b/test-suite/bugs/opened/3258.v
deleted file mode 100644
index 69a543044b..0000000000
--- a/test-suite/bugs/opened/3258.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Program Coq.Setoids.Setoid.
-
-Global Set Implicit Arguments.
-
-Hint Extern 0 => apply reflexivity : typeclass_instances.
-
-Inductive Comp : Type -> Type :=
-| Pick : forall A, (A -> Prop) -> Comp A.
-
-Axiom computes_to : forall A, Comp A -> A -> Prop.
-
-Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
-
-Global Instance refine_PreOrder A : PreOrder (@refine A).
-Admitted.
-
-Add Parametric Morphism A
-: (@Pick A)
-    with signature
-    (pointwise_relation _ (flip impl))
-      ==> (@refine A)
-      as refine_flip_impl_Pick.
-  admit.
-Defined.
-Definition remove_forall_eq' A x B (P : A -> B -> Prop) : pointwise_relation _ impl (P x) (fun z => forall y : A, y = x -> P y z).
-  admit.
-Defined.
-Goal forall A B (x : A) (P : _ -> _ -> Prop),
-       refine (Pick (fun n : B => forall y, y = x -> P y n))
-              (Pick (fun n : B => P x n)).
-Proof.
-  intros.
-  setoid_rewrite (@remove_forall_eq' _ _ _ _).
-  Undo.
-  Fail setoid_rewrite (@remove_forall_eq' _ _ _).
-- 
cgit v1.2.3