test-suite/bugs/closed/bug_10560.v


1
2
3
4
5
6
7
8
9

From Coq Require Import Int63.
Open Scope int63_scope.

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