aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-15 15:07:04 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-01-15 15:07:04 -0500
commit3c99dc494a807354a48e5a2f0f78f7979706cb70 (patch)
treef4bf81af3ee14175321116028059cd56f5f6770a /src/Util
parente182d5eb9da76e202f6f8f040896c0dafdc539dd (diff)
Add StringMap
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/StringMap.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/StringMap.v b/src/Util/StringMap.v
new file mode 100644
index 000000000..8b45d81d4
--- /dev/null
+++ b/src/Util/StringMap.v
@@ -0,0 +1,7 @@
+Require Import Coq.FSets.FMapInterface.
+Require Import Coq.FSets.FMapList.
+Require Import Coq.Structures.OrderedType.
+Require Import Coq.Strings.String.
+Require Import Crypto.Util.Strings.String_as_OT.
+
+Module StringMap := FMapList.Make String_as_OT.