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

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

Merged
merged 1 commit into from
Sep 17, 2024
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.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions examples/ConsiderDemo.v
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
Require Import Coq.Bool.Bool.
Require Import Arith.PeanoNat.
From Coq Require Import Bool.
From Coq Require Import PeanoNat.
Require Import ExtLib.Tactics.Consider.
Require Import ExtLib.Data.Nat.

Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
From Coq Require Import ZArith.
From Coq Require Import Lia.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down
2 changes: 1 addition & 1 deletion theories/Core/Decision.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Import Coq.Classes.DecidableClass.
From Coq.Classes Require Import DecidableClass.

Check warning on line 1 in theories/Core/Decision.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Classes has been replaced by Stdlib.Classes.

Definition decideP (P : Prop) {D : Decidable P} : {P} + {~P} :=
match @Decidable_witness P D as X return (X = true -> P) -> (X = false -> ~P) -> {P} + {~P} with
Expand Down
4 changes: 2 additions & 2 deletions theories/Core/EquivDec.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Import Coq.Classes.EquivDec.
From Coq.Classes Require Import EquivDec.

Check warning on line 1 in theories/Core/EquivDec.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Classes has been replaced by Stdlib.Classes.

Theorem EquivDec_refl_left {T : Type} {c : EqDec T (@eq T)} :
forall (n : T), equiv_dec n n = left (refl_equal _).
Expand All @@ -9,4 +9,4 @@
reflexivity.
Qed.

Export Coq.Classes.EquivDec.
Export EquivDec.
2 changes: 1 addition & 1 deletion theories/Data/HList.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Import Coq.Lists.List Coq.Arith.PeanoNat.
From Coq Require Import List PeanoNat.
Require Import Relations RelationClasses.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Data.SigT.
Expand Down
5 changes: 2 additions & 3 deletions theories/Data/List.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
Require Import Coq.Lists.List.
Require Coq.Classes.EquivDec.
From Coq Require Import List EquivDec.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Structures.Reducible.
Expand All @@ -20,7 +19,7 @@ Section EqDec.
Proof.
red. unfold Equivalence.equiv, RelationClasses.complement.
intros.
change (x = y -> False) with (x <> y).
change (x = y -> False) with (not (x = y)).
decide equality. eapply EqDec_T.
Qed.
End EqDec.
Expand Down
6 changes: 3 additions & 3 deletions theories/Data/ListFirstnSkipn.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
From Coq.Lists Require Import List.
From Coq.ZArith Require Import ZArith.
From Coq.micromega Require Import Lia.

(** For backwards compatibility with hint locality attributes. *)
Set Warnings "-unsupported-attributes".
Expand Down
4 changes: 2 additions & 2 deletions theories/Data/ListNth.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Require Import Coq.Lists.List.
Require Import Coq.Arith.PeanoNat.
From Coq.Lists Require Import List.

Check warning on line 1 in theories/Data/ListNth.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Lists has been replaced by Stdlib.Lists.
From Coq.Arith Require Import PeanoNat.

Check warning on line 2 in theories/Data/ListNth.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Arith has been replaced by Stdlib.Arith.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down
2 changes: 1 addition & 1 deletion theories/Data/Nat.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Coq.Arith.Arith.
From Coq.Arith Require Arith.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Tactics.Consider.
Expand Down
4 changes: 2 additions & 2 deletions theories/Data/PreFun.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relations.
From Coq.Classes Require Import Morphisms.

Check warning on line 1 in theories/Data/PreFun.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Classes has been replaced by Stdlib.Classes.
From Coq.Relations Require Import Relations.

Check warning on line 2 in theories/Data/PreFun.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Coq.Relations has been replaced by Stdlib.Relations.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down
2 changes: 1 addition & 1 deletion theories/Data/SigT.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Coq.Classes.EquivDec.
From Coq.Classes Require EquivDec.
Require Import ExtLib.Structures.EqDep.
Require Import ExtLib.Tactics.Injection.
Require Import ExtLib.Tactics.EqDep.
Expand Down
4 changes: 1 addition & 3 deletions theories/Data/String.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
Require Import Coq.Strings.String.
Require Import Coq.Program.Program.
Require Import Coq.Arith.PeanoNat.
From Coq Require Import String Program PeanoNat.

Require Import ExtLib.Tactics.Consider.
Require Import ExtLib.Core.RelDec.
Expand Down Expand Up @@ -32,8 +30,8 @@
match l , r with
| Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
bool_cmp l8 r8 >> bool_cmp l7 r7 >> bool_cmp l6 r6 >> bool_cmp l5 r5 >>

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 33 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.
bool_cmp l4 r4 >> bool_cmp l3 r3 >> bool_cmp l2 r2 >> bool_cmp l1 r1

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.11)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.12)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.13)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.

Check warning on line 34 in theories/Data/String.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.19)

Notation bool_cmp is deprecated since 8.12.
end.

#[deprecated(since="8.15",note="Use Ascii.compare instead.")]
Expand Down
11 changes: 5 additions & 6 deletions theories/Programming/Show.v
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
Require Coq.Strings.Ascii.
Require Coq.Strings.String.
Require Import Coq.Strings.String.
Require Import Coq.Program.Wf.
Require Import Coq.PArith.BinPos.
Require Import Coq.ZArith.ZArith.
From Coq Require Ascii.
From Coq Require Import String.
From Coq.Program Require Import Wf.
From Coq Require Import BinPos.
From Coq Require Import ZArith.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Structures.Reducible.
Require Import ExtLib.Programming.Injection.
Expand Down
6 changes: 3 additions & 3 deletions theories/Recur/Measure.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Require Import Coq.Classes.RelationClasses.
Require Coq.Arith.Wf_nat.
From Coq.Classes Require Import RelationClasses.
From Coq.Arith Require Wf_nat.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down Expand Up @@ -34,4 +34,4 @@ Section measure.

Definition well_founded_mlt : well_founded mlt :=
@well_founded_compose T nat m lt Wf_nat.lt_wf.
End measure.
End measure.
8 changes: 4 additions & 4 deletions theories/Structures/EqDep.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Coq.Logic.Eqdep_dec.
From Coq.Logic Require Eqdep_dec.
Require EquivDec.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Tactics.Consider.
Expand All @@ -12,18 +12,18 @@ Section Classes.

Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
intros.
eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
Qed.

Theorem UIP_equal : forall {x y : A} (p1 p2 : x = y), p1 = p2.
eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
Qed.

Lemma inj_pair2 :
forall (P:A -> Type) (p:A) (x y:P p),
existT P p x = existT P p y -> x = y.
Proof.
intros. eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec; auto.
intros. eapply Eqdep_dec.inj_pair2_eq_dec; auto.
Qed.

Theorem equiv_dec_refl_left : forall a, @EquivDec.equiv_dec _ _ _ dec a a = left eq_refl.
Expand Down
2 changes: 1 addition & 1 deletion theories/Structures/FunctorLaws.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Require Import Coq.Relations.Relations.
From Coq.Relations Require Import Relations.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Structures.Functor.

Expand Down
4 changes: 2 additions & 2 deletions theories/Tactics/EqDep.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Require Import Coq.Classes.EquivDec.
From Coq.Classes Require Import EquivDec.
Require Import ExtLib.Structures.EqDep.
Require Coq.Logic.Eqdep_dec.
From Coq.Logic Require Eqdep_dec.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down
Loading