test-suite/bugs/closed/bug_12483.v


1
2
3
4
5
6
7
8
9
10

Require Import Floats.

Goal False.
Proof.
cut (false = true).
{ intro H; discriminate H. }
change false with (1 <=? 0)%float.
rewrite leb_spec.
Fail reflexivity.
Abort.