Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21851 #200

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

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

Adapt to https://github.com/rocq-prover/rocq/pull/21851 #200

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/Rewriter/Demo.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Require Import Rewriter.Util.plugins.RewriterBuild.
(** We will be working with examples involving arithmetic on [nat] and
[Z], as well as some examples on [list], so we import the relevant
files. *)
From Coq Require Import Arith ZArith List.
From Stdlib Require Import Arith ZArith List.
Import ListNotations. Local Open Scope list_scope.

(** We [Unset Ltac Backtrace] to get prettier error messages. *)
Expand Down
10 changes: 5 additions & 5 deletions src/Rewriter/Language/IdentifiersBasicGenerate.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import Morphisms.
From Coq Require Import List.
From Stdlib Require Import ZArith.
From Stdlib Require Import Bool.
From Stdlib Require Import Morphisms.
From Stdlib Require Import List.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Bool.
Require Import Ltac2.Printf.
Expand Down Expand Up @@ -30,7 +30,7 @@ Require Import Rewriter.Util.Tactics.PrintGoal.
Require Import Rewriter.Util.Tactics.CacheTerm.
Require Import Rewriter.Util.Tactics2.Notations.
Require Import Rewriter.Util.HProp.
Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
Import Stdlib.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.

Import EqNotations.
Module Compilers.
Expand Down
10 changes: 5 additions & 5 deletions src/Rewriter/Language/IdentifiersGenerate.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
From Coq Require Import ZArith.
From Coq Require Import FMapPositive.
From Coq Require Import MSetPositive.
From Coq Require Import List.
From Coq Require Import Derive.
From Stdlib Require Import ZArith.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import List.
From Stdlib Require Import Derive.
Require Import Rewriter.Util.CPSNotations.
Require Import Rewriter.Util.Option.
Require Import Rewriter.Util.PrimitiveSigma.
Expand Down
6 changes: 3 additions & 3 deletions src/Rewriter/Language/IdentifiersGenerateProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From Coq Require Import ZArith.
From Coq Require Import MSetPositive.
From Coq Require Import FMapPositive.
From Stdlib Require Import ZArith.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import FMapPositive.
Require Import Rewriter.Util.PrimitiveSigma.
Require Import Rewriter.Util.MSetPositive.Facts.
Require Import Rewriter.Util.CPSNotations.
Expand Down
12 changes: 6 additions & 6 deletions src/Rewriter/Language/IdentifiersLibrary.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
From Coq Require Import Bool.
From Coq Require Import ZArith.
From Coq Require Import FMapPositive.
From Coq Require Import MSetPositive.
From Coq Require Import List.
From Coq Require Import Derive.
From Stdlib Require Import Bool.
From Stdlib Require Import ZArith.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import List.
From Stdlib Require Import Derive.
Require Import Rewriter.Util.CPSNotations.
Require Import Rewriter.Util.Option.
Require Import Rewriter.Util.PrimitiveSigma.
Expand Down
6 changes: 3 additions & 3 deletions src/Rewriter/Language/IdentifiersLibraryProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From Coq Require Import ZArith.
From Coq Require Import MSetPositive.
From Coq Require Import FMapPositive.
From Stdlib Require Import ZArith.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import FMapPositive.
Require Import Rewriter.Util.PrimitiveSigma.
Require Import Rewriter.Util.MSetPositive.Facts.
Require Import Rewriter.Util.CPSNotations.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Language/Language.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
From Coq Require Import ZArith.
From Coq Require Import FMapPositive.
From Coq Require Import Bool.
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import Relation_Definitions.
From Stdlib Require Import ZArith.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import Bool.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Relation_Definitions.
Require Import Rewriter.Language.PreCommon.
Require Import Rewriter.Util.LetIn.
Require Import Rewriter.Util.ListUtil.
Expand All @@ -17,7 +17,7 @@ Require Import Rewriter.Util.Bool.
Require Import Rewriter.Util.ListUtil.
Require Import Rewriter.Util.Prod.
Require Import Rewriter.Util.Notations.
Import Coq.Lists.List ListNotations.
Import Stdlib.Lists.List ListNotations.
Export Language.PreCommon.

Local Set Primitive Projections.
Expand Down
2 changes: 1 addition & 1 deletion src/Rewriter/Language/PreLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
From Coq Require Import List.
From Stdlib Require Import List.
Require Import Rewriter.Language.Pre.
Require Import Rewriter.Util.Bool.
Require Import Rewriter.Util.NatUtil.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Language/Reify.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
From Coq Require Import ZArith.
From Coq Require Import FMapPositive.
From Coq Require Import Bool.
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import Relation_Definitions.
From Stdlib Require Import ZArith.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import Bool.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Relation_Definitions.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.
Require Import Rewriter.Language.PreCommon.
Expand Down Expand Up @@ -36,7 +36,7 @@ Require Import Rewriter.Util.Tactics2.DestCase.
Require Import Rewriter.Util.Tactics2.InstantiateEvar.
Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations.
Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance.
Import Coq.Lists.List ListNotations.
Import Stdlib.Lists.List ListNotations.
Export Language.PreCommon.

Local Set Primitive Projections.
Expand Down
8 changes: 4 additions & 4 deletions src/Rewriter/Language/UnderLetsProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import SetoidList.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import SetoidList.
Require Import Rewriter.Language.Language.
Require Import Rewriter.Language.Inversion.
Require Import Rewriter.Language.Wf.
Expand All @@ -15,7 +15,7 @@ Require Import Rewriter.Util.Tactics.SpecializeAllWays.
Require Import Rewriter.Util.Tactics.SpecializeBy.
Require Import Rewriter.Util.Tactics.SplitInContext.
Require Import Rewriter.Util.Tactics.SetoidSubst.
Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.

Import EqNotations.
Module Compilers.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Language/Wf.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
From Coq Require Import ZArith.
From Coq Require Import List.
From Coq Require Import Lia.
From Coq Require Import FMapPositive.
From Coq Require Import Morphisms.
From Coq Require Import Relations.
From Stdlib Require Import ZArith.
From Stdlib Require Import List.
From Stdlib Require Import Lia.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Relations.
Require Import Rewriter.Language.Language.
Require Import Rewriter.Language.Inversion.
Require Import Rewriter.Util.Tactics.BreakMatch.
Expand All @@ -29,7 +29,7 @@ Require Import Rewriter.Util.Equality.
Require Import Rewriter.Util.IffT.
Require Import Rewriter.Util.CPSNotations.
Require Import Rewriter.Util.Notations.
Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.

Import EqNotations.
Module Compilers.
Expand Down
2 changes: 1 addition & 1 deletion src/Rewriter/Rewriter/AllTactics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
From Coq Require Import Morphisms.
From Stdlib Require Import Morphisms.
Require Import Rewriter.Language.Pre.
Require Import Rewriter.Language.Language.
Require Import Rewriter.Language.Inversion.
Expand Down
6 changes: 3 additions & 3 deletions src/Rewriter/Rewriter/Examples.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** * Examples of Using the Rewriter *)
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import List.
From Stdlib Require Import ZArith.
From Stdlib Require Import Lia.
From Stdlib Require Import List.
Require Import Rewriter.Util.ListUtil.
Require Import Rewriter.Util.LetIn.
Require Import Rewriter.Util.Notations.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import QArith.
From Coq Require Import Orders.
From Coq Require Import Lia.
From Coq Require Import Bool.
From Coq Require Import Mergesort.
From Coq Require Export List.
From Coq Require Export ZArith.
From Stdlib Require Import QArith.
From Stdlib Require Import Orders.
From Stdlib Require Import Lia.
From Stdlib Require Import Bool.
From Stdlib Require Import Mergesort.
From Stdlib Require Export List.
From Stdlib Require Export ZArith.
Export ListNotations.

Global Set Printing Width 1000.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import String.
From Coq Require Import Lia.
From Coq Require Import ZArith.
From Coq Require Import QArith.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Import List.
From Stdlib Require Import String.
From Stdlib Require Import Lia.
From Stdlib Require Import ZArith.
From Stdlib Require Import QArith.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.
From Stdlib Require Import List.
Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
Require Rewriter.Rewriter.Examples.PerfTesting.Sample.
Expand Down
6 changes: 3 additions & 3 deletions src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.

Global Instance list_rect_Proper_dep_gen {A P} (RP : forall x : list A, P x -> P x -> Prop)
: Proper (RP nil ==> forall_relation (fun x => forall_relation (fun xs => RP xs ==> RP (cons x xs))) ==> forall_relation RP) (@list_rect A P) | 10.
Expand Down
16 changes: 8 additions & 8 deletions src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import Lia.
From Coq Require Import ZArith.
From Coq Require Import QArith.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Import String.
From Coq Require Import List.
From Stdlib Require Import Lia.
From Stdlib Require Import ZArith.
From Stdlib Require Import QArith.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.
From Stdlib Require Import String.
From Stdlib Require Import List.
Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
Require Import Rewriter.Util.plugins.RewriterBuild.
Expand Down Expand Up @@ -421,7 +421,7 @@ Ltac describe_goal nm :=

Ltac do_coq_rewrite _ := rewrite -> !Z.add_0_r.

From Coq Require Import ssreflect.
From Stdlib Require Import ssreflect.

Ltac do_ssr_rewrite _ := rewrite !Z.add_0_r.

Expand Down
20 changes: 10 additions & 10 deletions src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
(** Utility file for subsampling large distributions *)
From Coq Require Import String.
From Coq Require Import Orders.
From Coq Require Import Lia.
From Coq Require Import Bool.
From Coq Require Import Mergesort.
From Coq Require Import QArith Qround Qabs Qminmax.
From Coq Require Import NArith.
From Coq Require Import ZArith.
From Coq Require Import Arith.
From Coq Require Import List.
From Stdlib Require Import String.
From Stdlib Require Import Orders.
From Stdlib Require Import Lia.
From Stdlib Require Import Bool.
From Stdlib Require Import Mergesort.
From Stdlib Require Import QArith Qround Qabs Qminmax.
From Stdlib Require Import NArith.
From Stdlib Require Import ZArith.
From Stdlib Require Import Arith.
From Stdlib Require Import List.
Require Import Rewriter.Util.LetIn.
Import ListNotations.
Local Open Scope list_scope.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import QArith.
From Coq Require Import MSetPositive.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Export ZArith.
From Coq Require Import List.
From Coq Require Import String.
From Stdlib Require Import QArith.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.
From Stdlib Require Export ZArith.
From Stdlib Require Import List.
From Stdlib Require Import String.
Require Import Rewriter.Util.Prod.
Require Import Rewriter.Util.Bool.Reflect.
Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import Lia.
From Coq Require Import ZArith.
From Coq Require Import QArith.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Import List.
From Coq Require Import String.
From Stdlib Require Import Lia.
From Stdlib Require Import ZArith.
From Stdlib Require Import QArith.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.
From Stdlib Require Import List.
From Stdlib Require Import String.
Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
Require Import Rewriter.Util.plugins.RewriterBuild.
Expand Down
8 changes: 4 additions & 4 deletions src/Rewriter/Rewriter/Examples/PrefixSums.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
(** * Examples of Using the Rewriter *)
From Coq Require Import Lia.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Import List.
From Stdlib Require Import Lia.
From Stdlib Require Import Morphisms.
From Stdlib Require Import Setoid.
From Stdlib Require Import List.
Require Import Rewriter.Util.LetIn.
Require Import Rewriter.Util.Notations.
Require Import Rewriter.Util.NatUtil.
Expand Down
14 changes: 7 additions & 7 deletions src/Rewriter/Rewriter/InterpProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import SetoidList.
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import MSetPositive.
From Coq Require Import FMapPositive.
From Stdlib Require Import ZArith.
From Stdlib Require Import Lia.
From Stdlib Require Import SetoidList.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import FMapPositive.
Require Import Rewriter.Language.Language.
Require Import Rewriter.Language.Inversion.
Require Import Rewriter.Language.Wf.
Expand Down
18 changes: 9 additions & 9 deletions src/Rewriter/Rewriter/ProofsCommon.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import SetoidList.
From Coq Require Import List.
From Coq Require Import Morphisms.
From Coq Require Import MSetPositive.
From Coq Require Import FMapPositive.
From Coq.Program Require Import Tactics.
From Stdlib Require Import ZArith.
From Stdlib Require Import Lia.
From Stdlib Require Import SetoidList.
From Stdlib Require Import List.
From Stdlib Require Import Morphisms.
From Stdlib Require Import MSetPositive.
From Stdlib Require Import FMapPositive.
From Stdlib Require Import Program.Tactics.
Require Import Rewriter.Language.Language.
Require Import Rewriter.Language.Inversion.
Require Import Rewriter.Language.Wf.
Expand Down Expand Up @@ -44,7 +44,7 @@ Require Import Rewriter.Util.Bool.
Require Import Rewriter.Util.NatUtil.
Require Rewriter.Util.InductiveHList.
Require Rewriter.Util.PrimitiveHList.
Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
Local Open Scope Z_scope.

Import EqNotations.
Expand Down
Loading
Loading