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

Jump to bottom

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

Merged
merged 1 commit into from
Sep 17, 2024
Merged

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

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/Common.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith Coq.Lists.SetoidList.
From Coq Require Import ZArith.ZArith SetoidList.
Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses
Coq.Program.Program Coq.Classes.Morphisms.
Require Export Fiat.Common.Tactics.SplitInContext.
Expand Down
2 changes: 1 addition & 1 deletion src/Common/Equality.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Import Coq.Lists.List Coq.Lists.SetoidList.
From Coq Require Import List SetoidList.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Strings.Ascii.
Expand Down
3 changes: 2 additions & 1 deletion src/Common/List/FlattenList.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
Require Import Coq.Lists.List Coq.Lists.SetoidList Fiat.Common.
From Coq Require Import List SetoidList.
Require Import Fiat.Common.
Require Import Coq.Arith.Arith.

Unset Implicit Arguments.
Expand Down
4 changes: 2 additions & 2 deletions src/Common/List/ListFacts.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Require Export Fiat.Common.Coq__8_4__8_5__Compat.
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool
Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.
From Coq Require Import List SetoidList Bool.
Require Import Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.

Unset Implicit Arguments.

Expand Down
2 changes: 1 addition & 1 deletion src/Common/List/PermutationFacts.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ Proof.
apply Permutation_length_1 in H; congruence.
Qed.

Require Import Coq.Lists.SetoidList.
From Coq Require Import SetoidList.

Lemma InA_app_swap {A} eqA :
Equivalence eqA
Expand Down
7 changes: 5 additions & 2 deletions src/Common/Wf.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
(** * Miscellaneous Well-Foundedness Facts *)
Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf.
Require Import Coq.Lists.SetoidList.
From Coq Require Import Setoid.
From Coq.Program Require Import Program Wf.
From Coq Require Import Wf_nat Morphisms.
From Coq.Init Require Import Wf.
From Coq Require Import SetoidList.
Require Import Coq.Arith.PeanoNat.
Require Export Fiat.Common.Coq__8_4__8_5__Compat.

Expand Down
2 changes: 1 addition & 1 deletion src/Computation/Decidable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ Global Program Instance bool_eq_Decidable {n m : bool} : Decidable (n = m) := {
Obligation 1. t' eqb_true_iff. Qed.

Require Import Coq.Strings.Ascii.
Require Import Coq.Bool.Sumbool.
From Coq Require Import Sumbool.

Global Program Instance ascii_eq_Decidable {n m : Ascii.ascii} :
Decidable (n = m) := {
Expand Down
Loading