test-suite/bugs/closed/bug_13276.v


1
2
3
4
5
6
7
8
9

From Coq Require Import Floats.
Open Scope float_scope.

Lemma foo :
  let n := opp 0 in sub n 0 = n.
Proof.
cbv.
apply eq_refl.
Qed.