aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/WeakListContext.v
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.