test-suite/bugs/closed/bug_1362.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(** Omega is now aware of the bodies of context variables
    (of type Z or nat). *)

Require Import ZArith Lia.
Open Scope Z.

Goal let x := 3 in x = 3.
intros.
lia.
Qed.

Open Scope nat.

Goal let x := 2 in x = 2.
intros.
lia.
Qed.