Skip to content

Commit c68d9e9

Browse files
proux01JasonGross
proux01
authored and
JasonGross
committed
1 parent 963487b commit c68d9e9

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+228
-228
lines changed

‎src/Rewriter/Demo.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Require Import Rewriter.Util.plugins.RewriterBuild.
99
(** We will be working with examples involving arithmetic on [nat] and
1010
[Z], as well as some examples on [list], so we import the relevant
1111
files. *)
12-
From Coq Require Import Arith ZArith List.
12+
From Stdlib Require Import Arith ZArith List.
1313
Import ListNotations. Local Open Scope list_scope.
1414

1515
(** We [Unset Ltac Backtrace] to get prettier error messages. *)

‎src/Rewriter/Language/IdentifiersBasicGenerate.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import Bool.
3-
From Coq Require Import Morphisms.
4-
From Coq Require Import List.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import Bool.
3+
From Stdlib Require Import Morphisms.
4+
From Stdlib Require Import List.
55
Require Import Ltac2.Ltac2.
66
Require Import Ltac2.Bool.
77
Require Import Ltac2.Printf.
@@ -30,7 +30,7 @@ Require Import Rewriter.Util.Tactics.PrintGoal.
3030
Require Import Rewriter.Util.Tactics.CacheTerm.
3131
Require Import Rewriter.Util.Tactics2.Notations.
3232
Require Import Rewriter.Util.HProp.
33-
Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
33+
Import Stdlib.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
3434

3535
Import EqNotations.
3636
Module Compilers.

‎src/Rewriter/Language/IdentifiersGenerate.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import FMapPositive.
3-
From Coq Require Import MSetPositive.
4-
From Coq Require Import List.
5-
From Coq Require Import Derive.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import FMapPositive.
3+
From Stdlib Require Import MSetPositive.
4+
From Stdlib Require Import List.
5+
From Stdlib Require Import Derive.
66
Require Import Rewriter.Util.CPSNotations.
77
Require Import Rewriter.Util.Option.
88
Require Import Rewriter.Util.PrimitiveSigma.

‎src/Rewriter/Language/IdentifiersGenerateProofs.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import MSetPositive.
3-
From Coq Require Import FMapPositive.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import MSetPositive.
3+
From Stdlib Require Import FMapPositive.
44
Require Import Rewriter.Util.PrimitiveSigma.
55
Require Import Rewriter.Util.MSetPositive.Facts.
66
Require Import Rewriter.Util.CPSNotations.

‎src/Rewriter/Language/IdentifiersLibrary.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
From Coq Require Import Bool.
2-
From Coq Require Import ZArith.
3-
From Coq Require Import FMapPositive.
4-
From Coq Require Import MSetPositive.
5-
From Coq Require Import List.
6-
From Coq Require Import Derive.
1+
From Stdlib Require Import Bool.
2+
From Stdlib Require Import ZArith.
3+
From Stdlib Require Import FMapPositive.
4+
From Stdlib Require Import MSetPositive.
5+
From Stdlib Require Import List.
6+
From Stdlib Require Import Derive.
77
Require Import Rewriter.Util.CPSNotations.
88
Require Import Rewriter.Util.Option.
99
Require Import Rewriter.Util.PrimitiveSigma.

‎src/Rewriter/Language/IdentifiersLibraryProofs.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import MSetPositive.
3-
From Coq Require Import FMapPositive.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import MSetPositive.
3+
From Stdlib Require Import FMapPositive.
44
Require Import Rewriter.Util.PrimitiveSigma.
55
Require Import Rewriter.Util.MSetPositive.Facts.
66
Require Import Rewriter.Util.CPSNotations.

‎src/Rewriter/Language/Language.v‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import FMapPositive.
3-
From Coq Require Import Bool.
4-
From Coq Require Import List.
5-
From Coq Require Import Morphisms.
6-
From Coq Require Import Relation_Definitions.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import FMapPositive.
3+
From Stdlib Require Import Bool.
4+
From Stdlib Require Import List.
5+
From Stdlib Require Import Morphisms.
6+
From Stdlib Require Import Relation_Definitions.
77
Require Import Rewriter.Language.PreCommon.
88
Require Import Rewriter.Util.LetIn.
99
Require Import Rewriter.Util.ListUtil.
@@ -17,7 +17,7 @@ Require Import Rewriter.Util.Bool.
1717
Require Import Rewriter.Util.ListUtil.
1818
Require Import Rewriter.Util.Prod.
1919
Require Import Rewriter.Util.Notations.
20-
Import Coq.Lists.List ListNotations.
20+
Import Stdlib.Lists.List ListNotations.
2121
Export Language.PreCommon.
2222

2323
Local Set Primitive Projections.

‎src/Rewriter/Language/PreLemmas.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
From Coq Require Import List.
1+
From Stdlib Require Import List.
22
Require Import Rewriter.Language.Pre.
33
Require Import Rewriter.Util.Bool.
44
Require Import Rewriter.Util.NatUtil.

‎src/Rewriter/Language/Reify.v‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
From Coq Require Import ZArith.
2-
From Coq Require Import FMapPositive.
3-
From Coq Require Import Bool.
4-
From Coq Require Import List.
5-
From Coq Require Import Morphisms.
6-
From Coq Require Import Relation_Definitions.
1+
From Stdlib Require Import ZArith.
2+
From Stdlib Require Import FMapPositive.
3+
From Stdlib Require Import Bool.
4+
From Stdlib Require Import List.
5+
From Stdlib Require Import Morphisms.
6+
From Stdlib Require Import Relation_Definitions.
77
Require Import Ltac2.Ltac2.
88
Require Import Ltac2.Printf.
99
Require Import Rewriter.Language.PreCommon.
@@ -36,7 +36,7 @@ Require Import Rewriter.Util.Tactics2.DestCase.
3636
Require Import Rewriter.Util.Tactics2.InstantiateEvar.
3737
Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations.
3838
Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance.
39-
Import Coq.Lists.List ListNotations.
39+
Import Stdlib.Lists.List ListNotations.
4040
Export Language.PreCommon.
4141

4242
Local Set Primitive Projections.

‎src/Rewriter/Language/UnderLetsProofs.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
From Coq Require Import List.
2-
From Coq Require Import Morphisms.
3-
From Coq Require Import SetoidList.
1+
From Stdlib Require Import List.
2+
From Stdlib Require Import Morphisms.
3+
From Stdlib Require Import SetoidList.
44
Require Import Rewriter.Language.Language.
55
Require Import Rewriter.Language.Inversion.
66
Require Import Rewriter.Language.Wf.
@@ -15,7 +15,7 @@ Require Import Rewriter.Util.Tactics.SpecializeAllWays.
1515
Require Import Rewriter.Util.Tactics.SpecializeBy.
1616
Require Import Rewriter.Util.Tactics.SplitInContext.
1717
Require Import Rewriter.Util.Tactics.SetoidSubst.
18-
Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
18+
Import Stdlib.Lists.List ListNotations. Local Open Scope list_scope.
1919

2020
Import EqNotations.
2121
Module Compilers.

0 commit comments

Comments
 (0)