summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-29 17:22:33 +0100
committerSon Ho2022-01-29 17:22:33 +0100
commit252a99fda7357c9389ffe9dd1bc1a039c9d0c0c1 (patch)
tree51a30f96b45006274704d41558d0328579caabbc
parent138083d6b17e25c774036231e16a784168dfb364 (diff)
Rename ExtractToFstar to ExtractToFStar
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml (renamed from src/ExtractToFstar.ml)0
-rw-r--r--src/main.ml2
2 files changed, 1 insertions, 1 deletions
diff --git a/src/ExtractToFstar.ml b/src/ExtractToFStar.ml
index 56a8c338..56a8c338 100644
--- a/src/ExtractToFstar.ml
+++ b/src/ExtractToFStar.ml
diff --git a/src/main.ml b/src/main.ml
index 1e402f54..e4c4dbd6 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -8,7 +8,7 @@ module EL = Easy_logging.Logging
module TA = TypesAnalysis
open PureToExtract
open ExtractAst
-open ExtractToFstar
+open ExtractToFStar
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.