blob: 6cafb9f0cd6ca1e21763942f7a86fae0b32b62d8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(** Omega is now aware of the bodies of context variables
(of type Z or nat). *)
Require Import ZArith Omega.
Open Scope Z.
Goal let x := 3 in x = 3.
intros.
omega.
Qed.
Open Scope nat.
Goal let x := 2 in x = 2.
intros.
omega.
Qed.
(** NB: this could be disabled for compatibility reasons *)
Unset Omega UseLocalDefs.
Goal let x := 4 in x = 4.
intros.
Fail omega.
Abort.
|
