aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ssr_clear.v
blob: 573ec47e0b89a82649783bcbee3682429a5351bc (plain)
1
2
3
4
5
6
Require Import ssreflect.

Example foo : True -> True.
Proof.
Fail move=> {NO_SUCH_NAME}.
Abort.