blob: f1c4a46e377e5c5ccdb4d47735bee8861733760f (
plain)
1
2
3
4
5
6
7
8
9
10
|
(** * Context made from an associative list *)
Require Import Coq.FSets.FMapWeakList.
Require Import Coq.FSets.FMapInterface.
Require Import Crypto.Compilers.Named.FMapContext.
Module WeakListContext (E : DecidableType).
Module WL := FMapWeakList.Make E.
Module Context := FMapContext WL.
Include Context.
End WeakListContext.
|