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.

Sign up for GitHub

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

Adapt to https://github.com/coq/coq/pull/19530 #51

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to https://github.com/coq/coq/pull/19530 #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/bbv/BinNotationZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Set Loose Hint Behavior "Strict".
Require Export bbv.BinNotation.
Require Export bbv.ReservedNotations.
Require Import Coq.ZArith.BinInt.
From Coq Require Import BinInt.

Notation "'Ob' a" := (Z.of_N (bin a)).

Expand Down
4 changes: 2 additions & 2 deletions src/bbv/DepEq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Set Loose Hint Behavior "Strict".
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Logic.Eqdep Coq.Logic.Eqdep_dec Coq.Program.Equality.
From Coq Require Import Peano_dec.
From Coq Require Import Eqdep Eqdep_dec Equality.

(** * Equalities on dependent types *)

Expand Down
2 changes: 1 addition & 1 deletion src/bbv/HexNotationZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Set Loose Hint Behavior "Strict".
Require Export bbv.HexNotation.
Require Export bbv.ReservedNotations.
Require Import Coq.ZArith.BinInt.
From Coq Require Import BinInt.

Notation "'Ox' a" := (Z.of_N (hex a)).

Expand Down
4 changes: 2 additions & 2 deletions src/bbv/N_Z_nat_conversions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Set Loose Hint Behavior "Strict".
(* This should be in the Coq library *)
Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Import Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
From Coq Require Import Arith NArith ZArith.
From Coq Require Import Lia.

Lemma N_to_Z_to_nat: forall (a: N), Z.to_nat (Z.of_N a) = N.to_nat a.
Proof.
Expand Down
10 changes: 5 additions & 5 deletions src/bbv/NatLib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
Set Loose Hint Behavior "Strict".
Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Import Coq.Arith.PeanoNat.Nat.
Require Import Coq.micromega.Lia.
Require Import Coq.NArith.NArith.
Require Import Coq.ZArith.ZArith.
From Coq Require Import Arith.
Import PeanoNat.Nat.
From Coq Require Import Lia.
From Coq Require Import NArith.
From Coq Require Import ZArith.
Require Import bbv.N_Z_nat_conversions.
Require Export bbv.Nomega.

Expand Down
4 changes: 2 additions & 2 deletions src/bbv/Nomega.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ Set Loose Hint Behavior "Strict".
(* Make [lia] work for [N] *)

Require Import Coq.Bool.Bool Coq.Classes.Morphisms.
Require Import Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith.
Require Import Coq.ZArith.ZArith.
From Coq Require Import Arith Lia NArith.
From Coq Require Import ZArith.

Local Open Scope N_scope.

Expand Down
14 changes: 7 additions & 7 deletions src/bbv/Word.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
Set Loose Hint Behavior "Strict".
(** Fixed precision machine words *)

Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.Equivalence Coq.Arith.PeanoNat Coq.ZArith.BinInt (* for hints *).
Require Import Coq.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith.
Require Import Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts.
Require Import Coq.Program.Tactics Coq.Program.Equality.
Require Import Coq.setoid_ring.Ring.
Require Import Coq.setoid_ring.Ring_polynom.
From Coq Require Import Morphisms Morphisms_Prop Equivalence PeanoNat BinInt (* for hints *).
From Coq Require Import Arith NArith Bool ZArith.
From Coq Require Import Eqdep_dec EqdepFacts.
From Coq.Program Require Import Tactics Equality.
From Coq Require Import Ring.
From Coq Require Import Ring_polynom.
Require Import bbv.Nomega.
Require Export bbv.ZLib bbv.NatLib bbv.NLib.
Require Export bbv.N_Z_nat_conversions.
Require Export bbv.DepEq bbv.DepEqNat.
Require Import bbv.ReservedNotations.

Require Import Coq.micromega.Lia.
From Coq Require Import Lia.
Local Existing Instances N.le_preorder Nat.add_wd Nat.div_wd Nat.divide_reflexive Nat.le_preorder Nat.le_wd Nat.lt_wd Nat.mod_wd Nat.mul_wd Nat.sub_wd Z.le_wd Z.le_preorder Z.lt_strorder.

Set Implicit Arguments.
Expand Down
2 changes: 1 addition & 1 deletion src/bbv/ZHints.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Set Loose Hint Behavior "Strict".
Require Import Coq.ZArith.ZArith.
From Coq Require Import ZArith.
Require Import bbv.ZLib.

(* Properties of the lemmas in this list:
Expand Down
8 changes: 4 additions & 4 deletions src/bbv/ZLib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
Set Loose Hint Behavior "Strict".
Require Import Coq.Classes.Morphisms.
Require Import Coq.ZArith.BinInt.
Import Coq.ZArith.BinInt.Z. (* for hints *)
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.ZArith.
From Coq Require Import BinInt.
Import BinInt.Z. (* for hints *)
From Coq Require Import Lia.
From Coq Require Import ZArith.

Local Open Scope Z_scope.

Expand Down
Loading