test-suite/ssr/noting_to_inject.v


1
2
3
4
5
6
7
8
9

Require Import ssreflect ssrfun ssrbool.


Goal forall b : bool, b -> False.
Set Warnings "+spurious-ssr-injection".
Fail move=> b [].
Set Warnings "-spurious-ssr-injection".
move=> b [].
Abort.