1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v
new file mode 100644
index 00000000..23d19e94
--- /dev/null
+++ b/test-suite/bugs/closed/3786.v
@@ -0,0 +1,33 @@
+Require Import TestSuite.admit.
+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.