aboutsummaryrefslogtreecommitdiff
path: root/test-suite/primitive/float/zero.v
blob: 75348d465709baa9005bbbc91bdb77810a5252bb (plain)
1
2
3
4
5
6
7
Require Import ZArith Int63 Floats.

Open Scope float_scope.

Fail Check (eq_refl : zero = neg_zero).
Fail Check (eq_refl <: zero = neg_zero).
Fail Check (eq_refl <<: zero = neg_zero).