diff options
Diffstat (limited to 'src/Compilers/Named/PositiveContext.v')
| -rw-r--r-- | src/Compilers/Named/PositiveContext.v | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/Compilers/Named/PositiveContext.v b/src/Compilers/Named/PositiveContext.v deleted file mode 100644 index 7b57098de..000000000 --- a/src/Compilers/Named/PositiveContext.v +++ /dev/null @@ -1,8 +0,0 @@ -Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Compilers.Named.FMapContext. - -Module PositiveContext := FMapContext PositiveMap. -Notation PositiveContext := PositiveContext.FMapContext. -Notation PositiveContext_nd := PositiveContext.FMapContext_nd. -Definition PositiveContextOk := PositiveContext.FMapContextOk (fun x y pf => pf). -Global Existing Instance PositiveContextOk. |