blob: 4356a174a7a0d9d47e93063ff9b2d9229a9c9f41 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Coq.FSets.FMapPositive.
Require Import Crypto.Reflection.Named.Syntax.
Require Import Crypto.Reflection.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.
|
