Adding test for bug #3786.

1 files changed, 2 insertions, 10 deletions

diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/closed/3786.v
index 5a1241151c..fd3bd7bd76 100644
--- a/test-suite/bugs/opened/3786.v
+++ b/test-suite/bugs/closed/3786.v
@@ -26,15 +26,7 @@ Definition sumUniqueImpl (ls : list nat)
 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.
+  try setoid_rewrite (@finite_set_handle_cardinal).
+Abort.