Fix the status of some resolved bugs

10 files changed, 26 insertions, 93 deletions

diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/closed/1501.v
index b36f21da1..e771e192d 100644
--- a/test-suite/bugs/opened/1501.v
+++ b/test-suite/bugs/closed/1501.v
@@ -3,6 +3,7 @@ Set Implicit Arguments.
 
 Require Export Relation_Definitions.
 Require Export Setoid.
+Require Import Morphisms.
 
 
 Section Essais.
@@ -40,57 +41,27 @@ Parameter
 
 Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
 
-Instance equiv_rel A: Equivalence (@equiv A).
-Proof.
- constructor.
- intros xa; apply equiv_refl.
- intros xa xb; apply equiv_sym.
- intros xa xb xc; apply equiv_trans.
-Defined.
-
-Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
-x)).
-
-Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y
-x.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
+Add Parametric Relation A : (K A) (@equiv A)
+    reflexivity proved by (@equiv_refl A)
+    symmetry proved by (@equiv_sym A)
+    transitivity proved by (@equiv_trans A)
+      as equiv_rel.
 
-Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
-fequiv
-y z -> fequiv x z.
+Add Parametric Morphism A B : (@bind A B)
+    with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B)
+      as bind_mor.
 Proof.
-  unfold fequiv; intros; eapply equiv_trans; auto with monad.
-Qed.
-
-Instance fequiv_re A B: Equivalence (@fequiv A B).
-Proof.
- constructor.
- intros f; apply fequiv_refl.
- intros f g; apply fequiv_sym.
- intros f g h; apply fequiv_trans.
-Defined.
-
-Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B).
-Proof.
- unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto.
+  unfold pointwise_relation; intros; apply bind_compat; auto.
 Qed.
 
 Lemma test:
   forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
- (equiv m1 m2) -> (equiv m2 m3) ->
-   equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
-         (bind m2 (fun a => bind m3 (fun a' => f a a'))).
+    (equiv m1 m2) -> (equiv m2 m3) ->
+    equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
+          (bind m2 (fun a => bind m3 (fun a' => f a a'))).
 Proof.
   intros A B m1 m2 m3 f H1 H2.
   setoid_rewrite H1. (* this works *)
-  Fail setoid_rewrite H2.
-Abort.
-(*  trivial by equiv_refl.
-Qed.*)
+  setoid_rewrite H2.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/closed/2456.v
index 5294adefd..e5a392c4d 100644
--- a/test-suite/bugs/opened/2456.v
+++ b/test-suite/bugs/closed/2456.v
@@ -50,4 +50,9 @@ Fail dependent destruction commute1;
 dependent destruction catchCommuteDetails;
 dependent destruction commute2;
 dependent destruction catchCommuteDetails generalizing X.
-Admitted.
+revert X.
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails.
+Abort.
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/closed/2814.v
index a740b4384..99da1e3e4 100644
--- a/test-suite/bugs/opened/2814.v
+++ b/test-suite/bugs/closed/2814.v
@@ -3,3 +3,4 @@ Require Import Program.
 Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
   intros.
   Fail induction H.
+Abort.
diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/closed/3100.v
index 6f35a74dc..6f35a74dc 100644
--- a/test-suite/bugs/opened/3100.v
+++ b/test-suite/bugs/closed/3100.v
diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/closed/3230.v
index 265310b1a..265310b1a 100644
--- a/test-suite/bugs/opened/3230.v
+++ b/test-suite/bugs/closed/3230.v
diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/closed/3320.v
index 05cf73281..0aac3c1b0 100644
--- a/test-suite/bugs/opened/3320.v
+++ b/test-suite/bugs/closed/3320.v
@@ -2,3 +2,4 @@ Goal forall x : nat, True.
   fix 1.
   assumption.
 Fail Qed.
+Undo.
diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v
deleted file mode 100644
index 3203afa13..000000000
--- a/test-suite/bugs/opened/3209.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Inductive eqT {A} (x : A) : A -> Type :=
-  reflT : eqT x x.
-Definition Bi_inv (A B : Type) (f : (A -> B)) :=
-  sigT (fun (g : B -> A) =>
-          sigT (fun (h : B -> A) =>
-                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
-                          forall a : A, eqT (h (f a)) a))).
-Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
-
-Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
-Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
-  sigT_rect (fun _ => TEquiv A B)
-            (fun (f : TEquiv A B -> eqT A B) H =>
-               sigT_rect (fun _ => TEquiv A B)
-                         (fun g _ => g e)
-                         H)
-            (UA A B).
diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v
deleted file mode 100644
index fd95503e6..000000000
--- a/test-suite/bugs/opened/3916.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import List.
-
-Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *)
diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v
deleted file mode 100644
index 5c4b4277b..000000000
--- a/test-suite/bugs/opened/3948.v
+++ /dev/null
@@ -1,25 +0,0 @@
-Module Type S.
-Parameter t : Type.
-End S.
-
-Module Bar(X : S).
-Proof.
-  Definition elt := X.t.
-  Axiom fold : elt.
-End Bar.
-
-Module Make (X: S) := Bar(X).
-
-Declare Module X : S.
-
-Module Type Interface.
-  Parameter constant : unit.
-End Interface.
-
-Module DepMap : Interface.
-  Module Dom := Make(X).
-  Definition constant : unit :=
-    let _ := @Dom.fold in tt.
-End DepMap.
-
-Print Assumptions DepMap.constant.
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
index b75170179..2ac553593 100644
--- a/test-suite/bugs/opened/4813.v
+++ b/test-suite/bugs/opened/4813.v
@@ -1,5 +1,5 @@
-(* An example one would like to see succeeding *)
+Require Import Program.Tactics.
 
 Record T := BT { t : Set }.
 Record U (x : T) := BU { u : t x -> Prop }.
-Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
+Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.