1 files changed, 0 insertions, 58 deletions
diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/opened/3344.v
deleted file mode 100644
index 8255fd6cce..0000000000
--- a/test-suite/bugs/opened/3344.v
+++ /dev/null
@@ -1,58 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *)
-Require Import Coq.Sets.Ensembles.
-Require Import Coq.Strings.String.
-Global Set Implicit Arguments.
-Global Set Asymmetric Patterns.
-Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end.
-
-Inductive Comp : Type -> Type :=
-| Return : forall A, A -> Comp A
-| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B.
-Inductive computes_to : forall A, Comp A -> A -> Prop :=
-| ReturnComputes : forall A v, @computes_to A (Return v) v
-| BindComputes : forall A B comp_a f comp_a_value comp_b_value,
-                   @computes_to A comp_a comp_a_value
-                   -> @computes_to B (f comp_a_value) comp_b_value
-                   -> @computes_to B (Bind comp_a f) comp_b_value.
-
-Inductive is_computational : forall A, Comp A -> Prop :=
-| Return_is_computational : forall A (x : A), is_computational (Return x)
-| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B),
-                            is_computational cA
-                            -> (forall a,
-                                  @computes_to _ cA a -> is_computational (f a))
-                            -> is_computational (Bind cA f).
-Theorem is_computational_inv A (c : Comp A)
-: is_computational c
-  -> match c with
-       | Return _ _ => True
-       | Bind _ _ x f => is_computational x
-                         /\ forall v, computes_to x v
-                                      -> is_computational (f v)
-     end.
-  admit.
-Defined.
-Fixpoint is_computational_unique_val A (c : Comp A) {struct c}
-: is_computational c -> { a | unique (computes_to c) a }.
-Proof.
-  refine match c as c return is_computational c -> { a | unique (computes_to c) a } with
-           | Return T x => fun _ => exist (unique (computes_to (Return x)))
-                                          x
-                                          _
-           | Bind _ _ x f
-             => fun H
-                => let H' := is_computational_inv H in
-                   let xv := @is_computational_unique_val _ _ (proj1 H') in
-                   let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in
-                   exist (unique (computes_to _))
-                         (proj1_sig fxv)
-                         _
-         end;
-  clearbodies;
-  clear is_computational_unique_val;
-  clear;
-  first [ abstract admit
-        | abstract admit ].
-(* [Fail] does not catch the anomaly *)
-Defined.
-(* Anomaly: Uncaught exception Not_found(_). Please report. *)