Skip to content

Commit e7a00b3

Browse files
authored
Merge pull request #42 from maximedenes/omega-lia
Prepare for porting to lia
2 parents 174889d + f911376 commit e7a00b3

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

examples/ConsiderDemo.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Require Import ExtLib.Tactics.Consider.
44
Require Import Coq.Bool.Bool.
55
Require Import ExtLib.Data.Nat.
66

7-
Require Import Coq.omega.Omega.
7+
Require Import Coq.ZArith.ZArith.
88

99
Set Implicit Arguments.
1010
Set Strict Implicit.

theories/Data/ListFirstnSkipn.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
Require Import Coq.Lists.List.
2-
Require Import Coq.omega.Omega.
2+
Require Import Coq.ZArith.ZArith.
33

44
Lemma firstn_app_L : forall T n (a b : list T),
55
n <= length a ->

0 commit comments

Comments
 (0)