Skip to content

Commit f911376

Browse files
committed
Prepare for porting to lia
This backward-compatible patch prepares ext-lib for rocq-prover/rocq#7878
1 parent a9c1389 commit f911376

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)