test-suite/ssr/rewrite_illtyped.v


1
2
3
4
5
6
7
8
9

From Coq Require Import ssreflect Setoid.

Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}.

Fact anomaly: forall P : SEProp, prop_of P.
Proof.
move=> [P E].
Fail rewrite E.
Abort.