ssr_clear.v « output « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/output/ssr_clear.v

blob: 573ec47e0b89a82649783bcbee3682429a5351bc (plain)

Require Import ssreflect.

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