summaryrefslogtreecommitdiff
path: root/src/ExtractToFStar.ml
diff options
context:
space:
mode:
authorSidney Congard2022-06-08 12:32:14 +0200
committerSidney Congard2022-06-08 12:32:14 +0200
commitba61ed50e7b2fdc78690de92d734a3747029f903 (patch)
treed038735ea4a263f80e1752661c1c707d21810f28 /src/ExtractToFStar.ml
parent1b3f5a15aaabf5810f07797550d1a19a55b6be3c (diff)
read globals from LLBC JSON into functions
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 0bbe591e..9766ddaf 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,6 +6,7 @@ open PureUtils
open TranslateCore
open PureToExtract
open StringUtils
+open FunIdentifier
module F = Format
(** A qualifier for a type definition.