bug_4462.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_4462.v

blob: be6d2bea768c107538a006c1035aee4651e4fd83 (plain)

Variables P Q : Prop.
Axiom pqrw : P <-> Q.

Require Setoid.

Goal P -> Q.
unshelve (rewrite pqrw).
Abort.