blob: 7b57098de5218b6e8fd50a08a1f977e371ce827a (
plain)
1
2
3
4
5
6
7
8
|
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.
|
