test-suite/success/bug_10890.v


1
2
3
4
5
6
7
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 *)