Skip to content

Commit

Permalink
Adapt to coq/coq#19530
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 authored and liyishuai committed Sep 17, 2024
1 parent 5ce96ab commit cbcd547
Show file tree
Hide file tree
Showing 16 changed files with 35 additions and 39 deletions.
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 @@ Proof.
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
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

0 comments on commit cbcd547

Please sign in to comment.