ssr_clear.v « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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.