From 26d9acf2418291ab740fedb91233e16445848ea1 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 25 Jan 2018 17:47:12 -0500
Subject: Fix the status of some resolved bugs

---
 test-suite/bugs/closed/1501.v | 67 ++++++++++++++++++++++++++++++
 test-suite/bugs/closed/2456.v | 58 ++++++++++++++++++++++++++
 test-suite/bugs/closed/2814.v |  6 +++
 test-suite/bugs/closed/3100.v |  9 ++++
 test-suite/bugs/closed/3230.v | 14 +++++++
 test-suite/bugs/closed/3320.v |  5 +++
 test-suite/bugs/opened/1501.v | 96 -------------------------------------------
 test-suite/bugs/opened/2456.v | 53 ------------------------
 test-suite/bugs/opened/2814.v |  5 ---
 test-suite/bugs/opened/3100.v |  9 ----
 test-suite/bugs/opened/3209.v | 17 --------
 test-suite/bugs/opened/3230.v | 14 -------
 test-suite/bugs/opened/3320.v |  4 --
 test-suite/bugs/opened/3916.v |  3 --
 test-suite/bugs/opened/3948.v | 25 -----------
 test-suite/bugs/opened/4813.v |  4 +-
 16 files changed, 161 insertions(+), 228 deletions(-)
 create mode 100644 test-suite/bugs/closed/1501.v
 create mode 100644 test-suite/bugs/closed/2456.v
 create mode 100644 test-suite/bugs/closed/2814.v
 create mode 100644 test-suite/bugs/closed/3100.v
 create mode 100644 test-suite/bugs/closed/3230.v
 create mode 100644 test-suite/bugs/closed/3320.v
 delete mode 100644 test-suite/bugs/opened/1501.v
 delete mode 100644 test-suite/bugs/opened/2456.v
 delete mode 100644 test-suite/bugs/opened/2814.v
 delete mode 100644 test-suite/bugs/opened/3100.v
 delete mode 100644 test-suite/bugs/opened/3209.v
 delete mode 100644 test-suite/bugs/opened/3230.v
 delete mode 100644 test-suite/bugs/opened/3320.v
 delete mode 100644 test-suite/bugs/opened/3916.v
 delete mode 100644 test-suite/bugs/opened/3948.v

diff --git a/test-suite/bugs/closed/1501.v b/test-suite/bugs/closed/1501.v
new file mode 100644
index 0000000000..e771e192dc
--- /dev/null
+++ b/test-suite/bugs/closed/1501.v
@@ -0,0 +1,67 @@
+Set Implicit Arguments.
+
+
+Require Export Relation_Definitions.
+Require Export Setoid.
+Require Import Morphisms.
+
+
+Section Essais.
+
+(* Parametrized Setoid *)
+Parameter K : Type -> Type.
+Parameter equiv : forall A : Type, K A -> K A -> Prop.
+Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
+Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
+Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
+-> equiv x z.
+
+(* basic operations *)
+Parameter val : forall A : Type, A -> K A.
+Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
+
+Parameter
+  bind_compat :
+    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
+    equiv m1 m2 ->
+    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
+
+(* monad axioms *)
+Parameter
+  bind_val_l :
+    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
+Parameter
+  bind_val_r :
+    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
+Parameter
+  bind_assoc :
+    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
+    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
+
+
+Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
+
+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.
+
+Add Parametric Morphism A B : (@bind A B)
+    with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B)
+      as bind_mor.
+Proof.
+  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'))).
+Proof.
+  intros A B m1 m2 m3 f H1 H2.
+  setoid_rewrite H1. (* this works *)
+  setoid_rewrite H2.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v
new file mode 100644
index 0000000000..e5a392c4d3
--- /dev/null
+++ b/test-suite/bugs/closed/2456.v
@@ -0,0 +1,58 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+Fail dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+revert X.
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails.
+Abort.
diff --git a/test-suite/bugs/closed/2814.v b/test-suite/bugs/closed/2814.v
new file mode 100644
index 0000000000..99da1e3e44
--- /dev/null
+++ b/test-suite/bugs/closed/2814.v
@@ -0,0 +1,6 @@
+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/closed/3100.v b/test-suite/bugs/closed/3100.v
new file mode 100644
index 0000000000..6f35a74dc1
--- /dev/null
+++ b/test-suite/bugs/closed/3100.v
@@ -0,0 +1,9 @@
+Fixpoint F (n : nat) (A : Type) : Type :=
+  match n with
+  | 0 => True
+  | S n => forall (x : A), F n (x = x)
+  end.
+
+Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
+intros A n.
+Fail change (forall x, F n (x = x)) with (F (S n)).
diff --git a/test-suite/bugs/closed/3230.v b/test-suite/bugs/closed/3230.v
new file mode 100644
index 0000000000..265310b1a3
--- /dev/null
+++ b/test-suite/bugs/closed/3230.v
@@ -0,0 +1,14 @@
+Structure type : Type := Pack { ob : Type }.
+Polymorphic Record category := { foo : Type }.
+Definition FuncComp := Pack category.
+Axiom C : category.
+
+Check (C : ob FuncComp). (* OK *)
+
+Canonical Structure FuncComp.
+
+Check (C : ob FuncComp).
+(* Toplevel input, characters 15-39:
+Error:
+The term "C" has type "category" while it is expected to have type
+ "ob FuncComp". *)
diff --git a/test-suite/bugs/closed/3320.v b/test-suite/bugs/closed/3320.v
new file mode 100644
index 0000000000..0aac3c1b06
--- /dev/null
+++ b/test-suite/bugs/closed/3320.v
@@ -0,0 +1,5 @@
+Goal forall x : nat, True.
+  fix 1.
+  assumption.
+Fail Qed.
+Undo.
diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/opened/1501.v
deleted file mode 100644
index b36f21da1b..0000000000
--- a/test-suite/bugs/opened/1501.v
+++ /dev/null
@@ -1,96 +0,0 @@
-Set Implicit Arguments.
-
-
-Require Export Relation_Definitions.
-Require Export Setoid.
-
-
-Section Essais.
-
-(* Parametrized Setoid *)
-Parameter K : Type -> Type.
-Parameter equiv : forall A : Type, K A -> K A -> Prop.
-Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
-Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
-Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
--> equiv x z.
-
-(* basic operations *)
-Parameter val : forall A : Type, A -> K A.
-Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
-
-Parameter
-  bind_compat :
-    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
-    equiv m1 m2 ->
-    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
-
-(* monad axioms *)
-Parameter
-  bind_val_l :
-    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
-Parameter
-  bind_val_r :
-    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
-Parameter
-  bind_assoc :
-    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
-    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
-
-
-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.
-
-Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
-fequiv
-y z -> fequiv x z.
-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.
-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'))).
-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.*)
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
deleted file mode 100644
index 5294adefd3..0000000000
--- a/test-suite/bugs/opened/2456.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-Require Import Equality.
-
-Parameter Patch : nat -> nat -> Set.
-
-Inductive Catch (from to : nat) : Type
-    := MkCatch : forall (p : Patch from to),
-                 Catch from to.
-Arguments MkCatch [from to].
-
-Inductive CatchCommute5
-        : forall {from mid1 mid2 to : nat},
-          Catch from mid1
-       -> Catch mid1 to
-       -> Catch from mid2
-       -> Catch mid2 to
-       -> Prop
-     := MkCatchCommute5 :
-           forall {from mid1 mid2 to : nat}
-                  (p : Patch from mid1)
-                  (q : Patch mid1 to)
-                  (q' : Patch from mid2)
-                  (p' : Patch mid2 to),
-           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
-
-Inductive CatchCommute {from mid1 mid2 to : nat}
-                       (p : Catch from mid1)
-                       (q : Catch mid1 to)
-                       (q' : Catch from mid2)
-                       (p' : Catch mid2 to)
-                     : Prop
-    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
-                         CatchCommute p q q' p'.
-Notation "<< p , q >> <~> << q' , p' >>"
-    := (CatchCommute p q q' p')
-    (at level 60, no associativity).
-
-Lemma CatchCommuteUnique2 :
-      forall {from mid mid' to : nat}
-             {p   : Catch from mid}  {q   : Catch mid  to}
-             {q'  : Catch from mid'} {p'  : Catch mid' to}
-             {q'' : Catch from mid'} {p'' : Catch mid' to}
-             (commute1 : <<p, q>> <~> <<q', p'>>)
-             (commute2 : <<p, q>> <~> <<q'', p''>>),
-      (p' = p'') /\ (q' = q'').
-Proof with auto.
-intros.
-set (X := commute2).
-Fail dependent destruction commute1;
-dependent destruction catchCommuteDetails;
-dependent destruction commute2;
-dependent destruction catchCommuteDetails generalizing X.
-Admitted.
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v
deleted file mode 100644
index a740b4384d..0000000000
--- a/test-suite/bugs/opened/2814.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Import Program.
-
-Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
-  intros.
-  Fail induction H.
diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/opened/3100.v
deleted file mode 100644
index 6f35a74dc1..0000000000
--- a/test-suite/bugs/opened/3100.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Fixpoint F (n : nat) (A : Type) : Type :=
-  match n with
-  | 0 => True
-  | S n => forall (x : A), F n (x = x)
-  end.
-
-Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
-intros A n.
-Fail change (forall x, F n (x = x)) with (F (S n)).
diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v
deleted file mode 100644
index 3203afa139..0000000000
--- 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/3230.v b/test-suite/bugs/opened/3230.v
deleted file mode 100644
index 265310b1a3..0000000000
--- a/test-suite/bugs/opened/3230.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Structure type : Type := Pack { ob : Type }.
-Polymorphic Record category := { foo : Type }.
-Definition FuncComp := Pack category.
-Axiom C : category.
-
-Check (C : ob FuncComp). (* OK *)
-
-Canonical Structure FuncComp.
-
-Check (C : ob FuncComp).
-(* Toplevel input, characters 15-39:
-Error:
-The term "C" has type "category" while it is expected to have type
- "ob FuncComp". *)
diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/opened/3320.v
deleted file mode 100644
index 05cf73281d..0000000000
--- a/test-suite/bugs/opened/3320.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Goal forall x : nat, True.
-  fix 1.
-  assumption.
-Fail Qed.
diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v
deleted file mode 100644
index fd95503e6b..0000000000
--- 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 5c4b4277b2..0000000000
--- 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 b75170179b..2ac5535934 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.
-- 
cgit v1.2.3