Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

remove all references to deprecated Arith modules from genarg tests #365

Merged
merged 1 commit into from
Oct 18, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
7 changes: 3 additions & 4 deletions tests/genarg/functional_induction.v
Original file line number Diff line number Diff line change
@@ -1,23 +1,22 @@
Set Implicit Arguments.

Require Import Arith.
Require Import Div2.
Require Import Recdef.

Function ceil_log2_S (n: nat) {wf lt n}: nat :=
match n with
| 0 => 0
| S _ => S (ceil_log2_S (div2 n))
| S _ => S (ceil_log2_S (Nat.div2 n))
end.
Proof.
intros.
apply lt_div2; auto with arith.
apply Nat.lt_div2; auto with arith.
apply lt_wf.
Defined.

Lemma ceil_log2_S_def n: ceil_log2_S n =
match n with
| 0 => 0
| S _ => S (ceil_log2_S (div2 n))
| S _ => S (ceil_log2_S (Nat.div2 n))
end.
Proof. functional induction (ceil_log2_S n); auto. Qed.
2 changes: 1 addition & 1 deletion tests/genarg/mbid.v
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
*)

Require Export NumPrelude NZAxioms.
Require Import NZBase NZOrder NZAddOrder Plus Minus.
Require Import NZBase NZOrder NZAddOrder.

(** In this file, we investigate the shape of domains satisfying
the [NZDomainSig] interface. In particular, we define a
Expand Down
2 changes: 1 addition & 1 deletion tests/genarg/setoid_rewrite.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Require Setoid.
Require Import PeanoNat Le Gt Minus Bool Lt List.
Require Import PeanoNat Bool List.
Require Import Lia.

Section ReDun.
Expand Down