From 34e69c881e72466e31c30b4d7ec6881d54f55a45 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 9 Jul 2020 16:09:35 +0200
Subject: Add test for #10890 derive vs abstract

---
 test-suite/success/bug_10890.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/success/bug_10890.v

diff --git a/test-suite/success/bug_10890.v b/test-suite/success/bug_10890.v
new file mode 100644
index 0000000000..37b6c816cc
--- /dev/null
+++ b/test-suite/success/bug_10890.v
@@ -0,0 +1,8 @@
+Require Import Derive.
+
+Derive foo SuchThat (foo = foo :> nat) As bar.
+Proof.
+  Unshelve.
+  2:abstract exact 0.
+   exact eq_refl.
+Defined. (* or Qed: anomaly kernel doesn't support existential variables *)
-- 
cgit v1.2.3