1 files changed, 58 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3344.v b/test-suite/bugs/closed/3344.v
new file mode 100644
index 00000000..8255fd6c
--- /dev/null
+++ b/test-suite/bugs/closed/3344.v
@@ -0,0 +1,58 @@
+(* 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. *)