From b8efac9f2cadbc0f700408fcb6f8187ef6527fd9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Feb 2015 20:04:29 +0100
Subject: Adding test for bug #3786.

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

diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v
new file mode 100644
index 0000000000..fd3bd7bd76
--- /dev/null
+++ b/test-suite/bugs/closed/3786.v
@@ -0,0 +1,32 @@
+Require Coq.Lists.List.
+Require Coq.Sets.Ensembles.
+Import Coq.Sets.Ensembles.
+Global Set Implicit Arguments.
+Delimit Scope comp_scope with comp.
+Inductive Comp : Type -> Type :=
+| Return : forall A, A -> Comp A
+| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B
+| Pick : forall A, Ensemble A -> Comp A.
+Notation ret := Return.
+Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp))
+                           (at level 81, right associativity,
+                            format "'[v' x  <-  y ; '/' z ']'") : comp_scope.
+Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
+Open Scope comp.
+Axiom elements : forall {A} (ls : list A), Ensemble A.
+Axiom to_list : forall {A} (S : Ensemble A), Comp (list A).
+Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0).
+Definition sumUniqueSpec (ls : list nat) : Comp nat.
+  exact (ls' <- to_list (elements ls);
+         List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls').
+Defined.
+Axiom admit : forall {T}, T.
+Definition sumUniqueImpl (ls : list nat)
+: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type.
+Proof.
+  eexists.
+  match goal with
+    | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
+  end.
+  try setoid_rewrite (@finite_set_handle_cardinal).
+Abort.
diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/opened/3786.v
deleted file mode 100644
index 5a1241151c..0000000000
--- a/test-suite/bugs/opened/3786.v
+++ /dev/null
@@ -1,40 +0,0 @@
-Require Coq.Lists.List.
-Require Coq.Sets.Ensembles.
-Import Coq.Sets.Ensembles.
-Global Set Implicit Arguments.
-Delimit Scope comp_scope with comp.
-Inductive Comp : Type -> Type :=
-| Return : forall A, A -> Comp A
-| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B
-| Pick : forall A, Ensemble A -> Comp A.
-Notation ret := Return.
-Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp))
-                           (at level 81, right associativity,
-                            format "'[v' x  <-  y ; '/' z ']'") : comp_scope.
-Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
-Open Scope comp.
-Axiom elements : forall {A} (ls : list A), Ensemble A.
-Axiom to_list : forall {A} (S : Ensemble A), Comp (list A).
-Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0).
-Definition sumUniqueSpec (ls : list nat) : Comp nat.
-  exact (ls' <- to_list (elements ls);
-         List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls').
-Defined.
-Axiom admit : forall {T}, T.
-Definition sumUniqueImpl (ls : list nat)
-: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type.
-Proof.
-  eexists.
-  match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b)
-  end;
-  try setoid_rewrite (@finite_set_handle_cardinal).
-  Undo.
-  match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
-  end.
-  try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
-Please report. *)
-  instantiate (1 := admit).
-  admit.
-Defined.
-- 
cgit v1.2.3