diff --git a/mk/boot.mk b/mk/boot.mk
index 8b5edc5ab..140e8141c 100644
--- a/mk/boot.mk
+++ b/mk/boot.mk
@@ -53,6 +53,7 @@ FSTAR = $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 %$(EXTENSION):
 	$(call msg, $(MSG), $(FF))
 	$(FSTAR) --already_cached ',*' $<
+	touch -c $@
 
 %.ml: FF=$(notdir $(subst $(EXTENSION),,$<))
 %.ml: MM=$(basename $(FF))
diff --git a/mk/extraction.mk b/mk/extraction.mk
index d2e4283ff..d9231c1bf 100644
--- a/mk/extraction.mk
+++ b/mk/extraction.mk
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+ExtractPulse,+ExtractPulseC,+ExtractPulseOCaml'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'Prims,FStarC'
 
diff --git a/mk/syntax_extension.mk b/mk/syntax_extension.mk
index dea234862..80c9f6691 100644
--- a/mk/syntax_extension.mk
+++ b/mk/syntax_extension.mk
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+PulseSyntaxExtension'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'Prims,FStarC'
 
diff --git a/pulse2rust/src/Makefile b/pulse2rust/src/Makefile
index edf2fa18a..49192a9c8 100644
--- a/pulse2rust/src/Makefile
+++ b/pulse2rust/src/Makefile
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+Pulse2Rust'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'FStarC'
 
diff --git a/pulse2rust/src/Pulse2Rust.Deps.fst b/pulse2rust/src/Pulse2Rust.Deps.fst
index 42738642a..06907f600 100644
--- a/pulse2rust/src/Pulse2Rust.Deps.fst
+++ b/pulse2rust/src/Pulse2Rust.Deps.fst
@@ -17,10 +17,9 @@
 module Pulse2Rust.Deps
 
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env
diff --git a/pulse2rust/src/Pulse2Rust.Deps.fsti b/pulse2rust/src/Pulse2Rust.Deps.fsti
index 5c49dc9b3..d561602fc 100644
--- a/pulse2rust/src/Pulse2Rust.Deps.fsti
+++ b/pulse2rust/src/Pulse2Rust.Deps.fsti
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Deps
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env
diff --git a/pulse2rust/src/Pulse2Rust.Env.fst b/pulse2rust/src/Pulse2Rust.Env.fst
index 6f8c72f5e..ba6ad0078 100644
--- a/pulse2rust/src/Pulse2Rust.Env.fst
+++ b/pulse2rust/src/Pulse2Rust.Env.fst
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Env
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open FStarC.Class.Setlike
 
diff --git a/pulse2rust/src/Pulse2Rust.Env.fsti b/pulse2rust/src/Pulse2Rust.Env.fsti
index a7dcb6fac..1f013f539 100644
--- a/pulse2rust/src/Pulse2Rust.Env.fsti
+++ b/pulse2rust/src/Pulse2Rust.Env.fsti
@@ -16,10 +16,10 @@
 
 module Pulse2Rust.Env
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
index 6a85a8a53..ea01c99c2 100644
--- a/pulse2rust/src/Pulse2Rust.Extract.fst
+++ b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -16,10 +16,10 @@
 
 module Pulse2Rust.Extract
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env
@@ -73,7 +73,7 @@ let lookup_datacon (g:env) (s:S.mlident) : option (list string & S.mlsymbol) =
     let ropt = find_map decls (lookup_datacon_in_module1 s) in
     match ropt with
     | None -> None
-    | Some tname -> Some (FStarC.Compiler.Util.split k ".", tname)
+    | Some tname -> Some (FStarC.Util.split k ".", tname)
   )
 
 //
@@ -887,7 +887,7 @@ let extract_generic_type_param_trait_bounds (attrs:list S.mlexpr) : list (list s
                       match e.expr with
                       | MLE_Const (MLC_String s) -> s
                       | _ -> failwith "unexpected generic type param bounds")
-         |> List.map (fun bound -> FStarC.Compiler.Util.split bound "::"))
+         |> List.map (fun bound -> FStarC.Util.split bound "::"))
   |> dflt []
 
 let extract_generic_type_params (tyvars:list S.ty_param)
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fsti b/pulse2rust/src/Pulse2Rust.Extract.fsti
index 579f082db..9522e754d 100644
--- a/pulse2rust/src/Pulse2Rust.Extract.fsti
+++ b/pulse2rust/src/Pulse2Rust.Extract.fsti
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Extract
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env
diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst
index 1f774e1f2..dc7885352 100644
--- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst
+++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst
@@ -16,9 +16,9 @@
 
 module Pulse2Rust.Rust.Syntax
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
-module L = FStarC.Compiler.List
+module L = FStarC.List
 
 let vec_new_fn = "vec_new"
 let panic_fn = "panic"
diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti
index 3365fb17a..a9bd3c451 100644
--- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti
+++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti
@@ -16,7 +16,7 @@
 
 module Pulse2Rust.Rust.Syntax
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 type lit_int_width =
   | I8
diff --git a/pulse2rust/src/Pulse2Rust.fst b/pulse2rust/src/Pulse2Rust.fst
index efe883d8f..7ef47e651 100644
--- a/pulse2rust/src/Pulse2Rust.fst
+++ b/pulse2rust/src/Pulse2Rust.fst
@@ -16,10 +16,10 @@
 
 module Pulse2Rust
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Deps
 open Pulse2Rust.Rust.Syntax
@@ -182,7 +182,7 @@ let extract (files:list string) (odir:string) (libs:string) : unit =
   let root_module = file_to_module_name (let root_file::_ = files in root_file) in
   // print1 "root_module: %s\n" root_module;
   let reachable_defs = collect_reachable_defs d root_module in
-  let external_libs = FStarC.Compiler.Util.split libs "," |> List.map trim_string in
+  let external_libs = FStarC.Util.split libs "," |> List.map trim_string in
   let g = empty_env external_libs d all_modules reachable_defs in
   let _, all_rust_files = List.fold_left (fun (g, all_rust_files) f ->
     // print1 "Extracting file: %s\n" f;
diff --git a/pulse2rust/src/Pulse2Rust.fst.config.json b/pulse2rust/src/Pulse2Rust.fst.config.json
index 0c25a1a14..cdd1786cc 100644
--- a/pulse2rust/src/Pulse2Rust.fst.config.json
+++ b/pulse2rust/src/Pulse2Rust.fst.config.json
@@ -4,7 +4,7 @@
     "--query_cache",
     "--lax",
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--with_fstarc",
     "--z3version",
     "4.13.3",
diff --git a/pulse2rust/src/RustBindings.fsti b/pulse2rust/src/RustBindings.fsti
index 2b6cc1f9b..d35bf1e28 100644
--- a/pulse2rust/src/RustBindings.fsti
+++ b/pulse2rust/src/RustBindings.fsti
@@ -16,7 +16,7 @@
 
 module RustBindings
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 
diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
index 277a82d67..e87da9c7e 100644
--- a/src/extraction/ExtractPulse.fst
+++ b/src/extraction/ExtractPulse.fst
@@ -1,20 +1,17 @@
 module ExtractPulse
 friend FStarC.Extraction.Krml
 
-(* IMPORTANT: these `open` directives come from FStarC.Extraction.Krml.
-   Without them, spurious dependencies on F* ulib will be introduced *)
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-open FStar
-open FStarC.Compiler
-open FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.List
+open FStarC.Util
 open FStarC.Extraction
 open FStarC.Extraction.ML
 open FStarC.Extraction.ML.Syntax
 open FStarC.Const
 open FStarC.BaseTypes
 
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 module FC = FStarC.Const
 
 open FStarC.Class.Show
diff --git a/src/extraction/ExtractPulseC.fst b/src/extraction/ExtractPulseC.fst
index 185e475f2..6c02c452a 100644
--- a/src/extraction/ExtractPulseC.fst
+++ b/src/extraction/ExtractPulseC.fst
@@ -1,11 +1,10 @@
 module ExtractPulseC
 
 friend FStarC.Extraction.Krml
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-open FStar
-open FStarC.Compiler
-open FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.List
+open FStarC.Util
 open FStarC.Extraction
 open FStarC.Extraction.ML
 open FStarC.Extraction.ML.Syntax
@@ -13,7 +12,7 @@ open FStarC.Const
 open FStarC.BaseTypes
 open FStarC.Extraction.Krml
 module K = FStarC.Extraction.Krml
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 
 (* JL: TODO: in stdlib somewhere? *)
 let opt_bind (m: option 'a) (k: 'a -> option 'b): option 'b =
@@ -26,7 +25,7 @@ let char_of_typechar (t: mlty): option char =
     if p = "Pulse.C.Typestring.cdot" then
       Some '.'
     else if BU.starts_with p "Pulse.C.Typestring.c" then
-      Some (FStarC.Compiler.String.get p (FStar.String.strlen "Pulse.C.Typestring.c"))
+      Some (FStarC.String.get p (FStar.String.strlen "Pulse.C.Typestring.c"))
     else
       None
 
diff --git a/src/extraction/ExtractPulseOCaml.fst b/src/extraction/ExtractPulseOCaml.fst
index 6049b5187..1fef29457 100644
--- a/src/extraction/ExtractPulseOCaml.fst
+++ b/src/extraction/ExtractPulseOCaml.fst
@@ -7,18 +7,17 @@ extract Quicksort.Task simply, without needing to build fstar.lib in
 OCaml 5. (We could.. but the compiled fstar.lib that F* comes with
 is in OCaml 4.X, so we'd need more build logic.) *)
 
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
+open FStarC.Effect
+open FStarC.List
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Util
+open FStarC.Util
 open FStarC.Extraction
 open FStarC.Extraction.ML
 open FStarC.Extraction.ML.Syntax
 open FStarC.Const
 open FStarC.BaseTypes
 
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 module FC = FStarC.Const
 
 open FStarC.Class.Show
diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
index 0c25a1a14..cdd1786cc 100644
--- a/src/extraction/Extraction.fst.config.json
+++ b/src/extraction/Extraction.fst.config.json
@@ -4,7 +4,7 @@
     "--query_cache",
     "--lax",
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--with_fstarc",
     "--z3version",
     "4.13.3",
diff --git a/src/ml/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly
index e40bf430b..7d6d83487 100644
--- a/src/ml/FStarC_Parser_Parse.mly
+++ b/src/ml/FStarC_Parser_Parse.mly
@@ -36,9 +36,9 @@ open Fstarcompiler
 open Prims
 open FStar_Pervasives
 open FStarC_Errors
-open FStarC_Compiler_List
-open FStarC_Compiler_Util
-open FStarC_Compiler_Range
+open FStarC_List
+open FStarC_Util
+open FStarC_Range
 
 (* TODO : these files should be deprecated and removed *)
 open FStarC_Parser_Const
diff --git a/src/ml/PulseSyntaxExtension_Parser.ml b/src/ml/PulseSyntaxExtension_Parser.ml
index db0ba258d..507464ea0 100644
--- a/src/ml/PulseSyntaxExtension_Parser.ml
+++ b/src/ml/PulseSyntaxExtension_Parser.ml
@@ -2,7 +2,7 @@ open Fstarcompiler
 open Lexing
 open FStar_Pervasives_Native
 open FStar_Pervasives
-open FStarC_Compiler_Range
+open FStarC_Range
 open FStarC_Parser_ParseIt
 module FP = FStarC_Parser_Parse
 module PP = Pulse_FStar_Parser
@@ -226,7 +226,7 @@ let parse_decl (s:string) (r:range) =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
+    let r = FStarC_Range.mk_range fn pos pos in
     Inr (Some ("Syntax error", r))
 
  
@@ -240,10 +240,10 @@ let parse_peek_id (s:string) (r:range) : (string, string * range) either =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
-    let msg = FStarC_Compiler_Util.format3 
+    let r = FStarC_Range.mk_range fn pos pos in
+    let msg = FStarC_Util.format3 
          "Failed to peek id, Syntax error @ %s\n%s\n%s\n"
-          (FStarC_Compiler_Range.string_of_range r)
+          (FStarC_Range.string_of_range r)
           (Printexc.to_string e)
           (Printexc.get_backtrace()) in
     Inr (msg, r)
@@ -263,5 +263,5 @@ let parse_lang (s:string) (r:range) =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
+    let r = FStarC_Range.mk_range fn pos pos in
     Inr (Some ("#lang-pulse: Syntax error", r))
diff --git a/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml b/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml
index b3f6a9dcc..763344119 100644
--- a/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml
+++ b/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml
@@ -5,7 +5,7 @@ open Pulse_Syntax_Base
 module U = Pulse_Syntax_Pure
 module S = FStarC_Syntax_Syntax
 type universe = Pulse_Syntax_Base.universe
-type range = FStarC_Compiler_Range.range
+type range = FStarC_Range.range
 let u_zero : universe = U.u_zero
 let u_succ (u:universe) : universe = U.u_succ u
 let u_var (s:string) : universe = U.u_var s
@@ -64,7 +64,7 @@ let tm_arrow (b:binder) (q:S.aqual) (body:comp) : term =
   U.tm_arrow b (map_aqual q) body
 let tm_expr (t:S.term) r : term = Pulse_Syntax_Pure.wr t r
 let tm_unknown r : term = wr r Tm_Unknown
-let tm_emp_inames :term = wr FStarC_Compiler_Range.dummyRange Tm_EmpInames
+let tm_emp_inames :term = wr FStarC_Range.dummyRange Tm_EmpInames
 let tm_add_inv (names:term) (n:term) r : term =
   Pulse_RuntimeUtils.set_range (Pulse_Syntax_Pure.tm_add_inv names n) r
 
@@ -231,7 +231,7 @@ let binder_to_string (env:Env.env) (b:binder)
   = tac_to_string env (Pulse_Syntax_Printer.binder_to_string b)
 let bv_to_string (x:bv) : string =
     x.bv_ppname.name ^ "@" ^
-     (FStarC_Compiler_Util.string_of_int x.bv_index)
+     (FStarC_Util.string_of_int x.bv_index)
 let term_to_string (env:Env.env) (t:term)
   : string
   = tac_to_string env (Pulse_Syntax_Printer.term_to_string t)
diff --git a/src/ml/Pulse_Extract_CompilerLib.ml b/src/ml/Pulse_Extract_CompilerLib.ml
index 4c2429078..2476f6233 100644
--- a/src/ml/Pulse_Extract_CompilerLib.ml
+++ b/src/ml/Pulse_Extract_CompilerLib.ml
@@ -10,24 +10,24 @@ let unit_ty = S.t_unit
 let mk_return (t:term) : term =
   S.mk
     (S.Tm_meta {tm2=t; meta=S.Meta_monadic_lift (C.effect_PURE_lid, C.effect_DIV_lid, S.tun)})
-    FStarC_Compiler_Range.dummyRange
+    FStarC_Range.dummyRange
 let mk_meta_monadic (t: term): term =
   S.mk (S.Tm_meta {tm2=t; meta=S.Meta_monadic (C.effect_DIV_lid, S.tun)})
-    FStarC_Compiler_Range.dummyRange
+    FStarC_Range.dummyRange
 let mk_pure_let (b:binder) (head:term) (body:term) : term =
   let lb = U.mk_letbinding
-    (Inl b.binder_bv) [] b.binder_bv.sort C.effect_PURE_lid head [] FStarC_Compiler_Range.dummyRange in
-  S.mk (S.Tm_let {lbs=(false, [lb]); body1=body}) FStarC_Compiler_Range.dummyRange
+    (Inl b.binder_bv) [] b.binder_bv.sort C.effect_PURE_lid head [] FStarC_Range.dummyRange in
+  S.mk (S.Tm_let {lbs=(false, [lb]); body1=body}) FStarC_Range.dummyRange
 let mk_let (b:binder) (head:term) (body:term) : term =
   let lb = U.mk_letbinding
-    (Inl b.binder_bv) [] b.binder_bv.sort C.effect_DIV_lid head [] FStarC_Compiler_Range.dummyRange in
+    (Inl b.binder_bv) [] b.binder_bv.sort C.effect_DIV_lid head [] FStarC_Range.dummyRange in
   let tm_let =
-    S.mk (S.Tm_let {lbs=(false, [lb]); body1=body}) FStarC_Compiler_Range.dummyRange in
-  S.mk (S.Tm_meta {tm2=tm_let; meta=S.Meta_monadic (C.effect_DIV_lid, S.tun)}) FStarC_Compiler_Range.dummyRange
+    S.mk (S.Tm_let {lbs=(false, [lb]); body1=body}) FStarC_Range.dummyRange in
+  S.mk (S.Tm_meta {tm2=tm_let; meta=S.Meta_monadic (C.effect_DIV_lid, S.tun)}) FStarC_Range.dummyRange
 let mk_if (b:term) (then_:term) (else_:term) : term =
   U.if_then_else b then_ else_
 
 let mk_extracted_as_attr (impl: term) : term =
   S.mk_Tm_app (S.tconst FStarC_Parser_Const.extract_as_lid)
-    [S.mk (S.Tm_quoted (impl, {qkind=S.Quote_static; antiquotations=(Prims.int_zero,[])})) FStarC_Compiler_Range.dummyRange, None]
-    FStarC_Compiler_Range.dummyRange
+    [S.mk (S.Tm_quoted (impl, {qkind=S.Quote_static; antiquotations=(Prims.int_zero,[])})) FStarC_Range.dummyRange, None]
+    FStarC_Range.dummyRange
diff --git a/src/ml/Pulse_RuntimeUtils.ml b/src/ml/Pulse_RuntimeUtils.ml
index ac9ef518d..957fd49a3 100644
--- a/src/ml/Pulse_RuntimeUtils.ml
+++ b/src/ml/Pulse_RuntimeUtils.ml
@@ -1,6 +1,6 @@
 open Fstarcompiler
-type context = ((string * FStarC_Compiler_Range.range option) list) (* FStar_Sealed.sealed *)
-let extend_context (s:string) (r:FStarC_Compiler_Range.range option) (c:context) = (s,r)::c
+type context = ((string * FStarC_Range.range option) list) (* FStar_Sealed.sealed *)
+let extend_context (s:string) (r:FStarC_Range.range option) (c:context) = (s,r)::c
 module TR = FStarC_Tactics_Result
 
 type ('a,'wp) tac_repr = FStarC_Tactics_Types.proofstate -> 'a TR.__result
@@ -10,7 +10,7 @@ let ctxt_elt_as_string (s, r) =
     match r with
     | None -> s
     | Some r ->
-      "@" ^ FStarC_Compiler_Range.string_of_range r ^ ": " ^ s
+      "@" ^ FStarC_Range.string_of_range r ^ ": " ^ s
 let rec print_context (c:context) : string utac =
   fun ps ->
     TR.Success (
@@ -24,7 +24,7 @@ let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
     | sr::tl ->
       with_context tl (fun _ ps ->
       FStarC_Errors.with_ctx (ctxt_elt_as_string sr) (fun _ -> f () ps)) ps
-let with_error_bound (r:FStarC_Compiler_Range.range) (f: unit -> 'a utac) : 'a utac =
+let with_error_bound (r:FStarC_Range.range) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     FStarC_Errors.with_error_bound r (fun _ -> f () ps)
 let disable_admit_smt_queries (f: unit -> 'a utac) : 'a utac =
@@ -44,28 +44,28 @@ let with_extv (k:string) (v:string) (f: unit -> 'a utac) : 'a utac =
 let env_set_context (g:FStarC_Reflection_Types.env) (c:context) = g
 let print_exn (e:exn) = Printexc.to_string e
 let debug_at_level_no_module (s:string) =
-  let r = FStarC_Compiler_Debug.get_toggle s in
+  let r = FStarC_Debug.get_toggle s in
   !r
 let debug_at_level (g:FStarC_Reflection_Types.env) (s:string) =
-  let r = FStarC_Compiler_Debug.get_toggle s in
+  let r = FStarC_Debug.get_toggle s in
   !r
 
 let next_id () = FStarC_GenSym.next_id ()
-let bv_set_range (bv:FStarC_Syntax_Syntax.bv) (r:FStarC_Compiler_Range.range) = FStarC_Syntax_Syntax.set_range_of_bv bv r
+let bv_set_range (bv:FStarC_Syntax_Syntax.bv) (r:FStarC_Range.range) = FStarC_Syntax_Syntax.set_range_of_bv bv r
 let bv_range (bv:FStarC_Syntax_Syntax.bv) = FStarC_Syntax_Syntax.range_of_bv bv
-let binder_set_range (b:FStarC_Syntax_Syntax.binder) (r:FStarC_Compiler_Range.range) =
+let binder_set_range (b:FStarC_Syntax_Syntax.binder) (r:FStarC_Range.range) =
     { b with FStarC_Syntax_Syntax.binder_bv = (bv_set_range b.FStarC_Syntax_Syntax.binder_bv r) }
 let binder_range (b:FStarC_Syntax_Syntax.binder) = bv_range b.FStarC_Syntax_Syntax.binder_bv
-let start_of_range (r:FStarC_Compiler_Range.range) =
-  let open FStarC_Compiler_Range in
+let start_of_range (r:FStarC_Range.range) =
+  let open FStarC_Range in
   mk_range (file_of_range r) (start_of_range r) (start_of_range r)
-  let set_range (t:FStarC_Syntax_Syntax.term) (r:FStarC_Compiler_Range.range) = { t with FStarC_Syntax_Syntax.pos = r}
-let set_use_range (t:FStarC_Syntax_Syntax.term) (r:FStarC_Compiler_Range.range) = FStarC_Syntax_Subst.set_use_range r t
+  let set_range (t:FStarC_Syntax_Syntax.term) (r:FStarC_Range.range) = { t with FStarC_Syntax_Syntax.pos = r}
+let set_use_range (t:FStarC_Syntax_Syntax.term) (r:FStarC_Range.range) = FStarC_Syntax_Subst.set_use_range r t
 let error_code_uninstantiated_variable () = FStarC_Errors.errno FStarC_Errors_Codes.Error_UninstantiatedUnificationVarInTactic
-let is_range_zero (r:FStarC_Compiler_Range.range) = r = FStarC_Compiler_Range.dummyRange
-let union_ranges (r0:FStarC_Compiler_Range.range) (r1:FStarC_Compiler_Range.range) = FStarC_Compiler_Range.union_ranges r0 r1
+let is_range_zero (r:FStarC_Range.range) = r = FStarC_Range.dummyRange
+let union_ranges (r0:FStarC_Range.range) (r1:FStarC_Range.range) = FStarC_Range.union_ranges r0 r1
 let range_of_term (t:FStarC_Syntax_Syntax.term) = t.FStarC_Syntax_Syntax.pos
-let env_set_range (e:FStarC_Reflection_Types.env) (r:FStarC_Compiler_Range.range) =
+let env_set_range (e:FStarC_Reflection_Types.env) (r:FStarC_Range.range) =
    FStarC_TypeChecker_Env.set_range e r
 
 let is_pulse_option_set (x:string) : bool =
@@ -88,7 +88,7 @@ let debug_subst (s:S.subst_elt list) (t:S.term) (r1:S.term) (r2:S.term) =
   else r1
   (*
   FStarC_Options.debug_at_level_no_module
-  let open FStarC_Compiler_Util in
+  let open FStarC_Util in
   if U.term_eq_dbg true r1 r2
   then r1
   else (
@@ -130,7 +130,7 @@ let deep_transform_to_unary_applications (t:S.term) =
       | Tm_app { hd; args=_::_::_ as args } -> (
         match (FStarC_Syntax_Util.un_uinst hd).n with
         | Tm_fvar fv
-          when FStarC_Compiler_List.existsb (S.fv_eq_lid fv) builtin_lids ->
+          when FStarC_List.existsb (S.fv_eq_lid fv) builtin_lids ->
           t
         | _ -> 
          List.fold_left (fun t arg -> { t with n = Tm_app {hd=t; args=[arg]} }) hd args
@@ -140,11 +140,11 @@ let deep_transform_to_unary_applications (t:S.term) =
 
 let deep_compress (t:S.term) = FStarC_Syntax_Compress.deep_compress_uvars t
 let map_seal (t:'a) (f:'a -> 'b) : 'b = f t
-let float_one = FStarC_Compiler_Util.float_of_string "1.0"
+let float_one = FStarC_Util.float_of_string "1.0"
 module TcEnv = FStarC_TypeChecker_Env
 module Free = FStarC_Syntax_Free
-module BU = FStarC_Compiler_Util
-module FlatSet = FStarC_Compiler_FlatSet
+module BU = FStarC_Util
+module FlatSet = FStarC_FlatSet
 
 let lax_check_term_with_unknown_universes (g:TcEnv.env) (e:S.term)
   : S.term option
diff --git a/src/ml/pulseparser.mly b/src/ml/pulseparser.mly
index dd48f32dc..509027062 100644
--- a/src/ml/pulseparser.mly
+++ b/src/ml/pulseparser.mly
@@ -9,9 +9,9 @@ open Fstarcompiler
 open Prims
 open FStar_Pervasives
 open FStarC_Errors
-open FStarC_Compiler_List
-open FStarC_Compiler_Util
-open FStarC_Compiler_Range
+open FStarC_List
+open FStarC_Util
+open FStarC_Range
 open FStarC_Options
 (* TODO : these files should be deprecated and removed *)
 open FStarC_Syntax_Syntax
diff --git a/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst b/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst
index fbb7305ec..3e5802fec 100644
--- a/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst
@@ -16,19 +16,19 @@
 
 module PulseSyntaxExtension.ASTBuilder
 open FStarC
-open FStarC.Compiler.Effect
+open FStarC.Effect
 open FStarC.Parser.AST
 open FStarC.Parser.AST.Util
 open FStarC.Ident
-module BU = FStarC.Compiler.Util
-module List = FStarC.Compiler.List
+module BU = FStarC.Util
+module List = FStarC.List
 module A = FStarC.Parser.AST
 module AU = FStarC.Parser.AST.Util
 module S = FStarC.Syntax.Syntax
 open FStar.List.Tot
 open FStarC.Const
 
-let r_ = FStarC.Compiler.Range.dummyRange
+let r_ = FStarC.Range.dummyRange
 
 #push-options "--warn_error -272" //intentional top-level effect
 let pulse_checker_tac = Ident.lid_of_path ["Pulse"; "Main"; "check_pulse"] r_
@@ -38,7 +38,7 @@ let tm t r = { tm=t; range=r; level=Un}
 
 let parse_decl_name
   : contents:string ->
-    FStarC.Compiler.Range.range ->
+    FStarC.Range.range ->
     either AU.error_message FStarC.Ident.ident
   = fun contents r ->
     match Parser.parse_peek_id contents r with
@@ -54,7 +54,7 @@ let lid_as_term ns r = str (Ident.string_of_lid ns) r
 
 let encode_open_namespaces_and_abbreviations
     (ctx:open_namespaces_and_abbreviations)
-    (r:FStarC.Compiler.Range.range)
+    (r:FStarC.Range.range)
 : term & term
 = let tm t = tm t r in
   let str s = str s r in
@@ -72,9 +72,9 @@ let encode_open_namespaces_and_abbreviations
   in
   namespaces, abbrevs
 
-let encode_range (r:FStarC.Compiler.Range.range)
+let encode_range (r:FStarC.Range.range)
 : term & term & term
-= let open FStarC.Compiler.Range in
+= let open FStarC.Range in
   let line = line_of_pos (start_of_range r) in
   let col = col_of_pos (start_of_range r) in
   str (file_of_range r) r, i line r, i col r
@@ -82,7 +82,7 @@ let encode_range (r:FStarC.Compiler.Range.range)
 let parse_decl
   : open_namespaces_and_abbreviations ->
     contents:string ->
-    FStarC.Compiler.Range.range ->
+    FStarC.Range.range ->
     either AU.error_message decl
   = fun ctx contents r ->
       let tm t = tm t r in
@@ -116,7 +116,7 @@ let maybe_report_error first_error decls =
   | None -> Inr decls
   | Some (raw_error, msg, r) ->
     let should_fail_on_error =
-      let file = FStarC.Compiler.Range.file_of_range r in
+      let file = FStarC.Range.file_of_range r in
       match FStarC.Parser.Dep.maybe_module_name_of_file file with
       | None -> false //don't report hard errors on <input>; we'll log them as warnings below
       | Some _ ->
@@ -135,7 +135,7 @@ let maybe_report_error first_error decls =
       Inr <| (decls @ [Inr <| FStarC.Parser.AST.(mk_decl Unparseable r [])])
     )
 open FStarC.Class.Show
-let parse_extension_lang (contents:string) (r:FStarC.Compiler.Range.range)
+let parse_extension_lang (contents:string) (r:FStarC.Range.range)
 : either AU.error_message (list decl)
 = match Parser.parse_lang contents r with
   | Inr None ->
@@ -203,8 +203,8 @@ let _ = register_extension_lang_parser "pulse" {parse_decls=parse_extension_lang
    
 module TcEnv = FStarC.TypeChecker.Env
 module D = PulseSyntaxExtension.Desugar
-module L = FStarC.Compiler.List
-module R = FStarC.Compiler.Range
+module L = FStarC.List
+module R = FStarC.Range
 module DsEnv = FStarC.Syntax.DsEnv
 let sugar_decl = PulseSyntaxExtension.Sugar.decl
 let desugar_pulse (env:TcEnv.env) 
@@ -228,8 +228,8 @@ let desugar_pulse_decl_callback
   match fst d with
   | Inr None -> //All errors were logged via the error API
     //Raise one final error at the start of the decl to stop further processing
-    let start = FStarC.Compiler.Range.start_of_range rng in
-    let rng = FStarC.Compiler.Range.mk_range (FStarC.Compiler.Range.file_of_range rng) start start in
+    let start = FStarC.Range.start_of_range rng in
+    let rng = FStarC.Range.mk_range (FStarC.Range.file_of_range rng) start start in
     FStarC.Errors.raise_error rng FStarC.Errors.Fatal_SyntaxError "Failed to desugar pulse declaration"
   | Inr (Some (msg, rng)) ->
     FStarC.Errors.raise_error rng FStarC.Errors.Fatal_SyntaxError msg
diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst
index a647479dd..cee84ed5a 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst
@@ -16,18 +16,18 @@
 
 module PulseSyntaxExtension.Desugar
 open FStarC
-open FStarC.Compiler.Effect
+open FStarC.Effect
 module Sugar = PulseSyntaxExtension.Sugar
 module SW = PulseSyntaxExtension.SyntaxWrapper
 module A = FStarC.Parser.AST
 module D = FStarC.Syntax.DsEnv
 module ToSyntax = FStarC.ToSyntax.ToSyntax
 module S = FStarC.Syntax.Syntax
-module L = FStarC.Compiler.List
+module L = FStarC.List
 module U = FStarC.Syntax.Util
 module SS = FStarC.Syntax.Subst
-module R = FStarC.Compiler.Range
-module BU = FStarC.Compiler.Util
+module R = FStarC.Range
+module BU = FStarC.Util
 module P =  FStarC.Syntax.Print
 module LR = PulseSyntaxExtension.TransformRValues
 
@@ -184,7 +184,7 @@ let desugar_term (env:env_t) (t:A.term)
 let desugar_term_opt (env:env_t) (t:option A.term)
   : err SW.term
   = match t with
-    | None -> return (SW.tm_unknown FStarC.Compiler.Range.dummyRange)
+    | None -> return (SW.tm_unknown FStarC.Range.dummyRange)
     | Some e -> desugar_term env e
 
 //
@@ -205,7 +205,7 @@ let idents_as_binders (env:env_t) (l:list ident)
            (BU.format1 "Identifiers (%s) not found, consider adding them as binders" s)
            (non_tick_idents |> L.hd |> Ident.range_of_id)
     else begin
-      let erased_tm = A.(mk_term (Var FStarC.Parser.Const.erased_lid) FStarC.Compiler.Range.dummyRange Un) in
+      let erased_tm = A.(mk_term (Var FStarC.Parser.Const.erased_lid) FStarC.Range.dummyRange Un) in
       let mk_ty i =
         let wild = A.(mk_term Wild (Ident.range_of_id i) Un) in
         A.(mkApp erased_tm [wild, A.Nothing] (Ident.range_of_id i)) in
diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fsti b/src/syntax_extension/PulseSyntaxExtension.Desugar.fsti
index af3bde73f..fcdb7ddfa 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fsti
+++ b/src/syntax_extension/PulseSyntaxExtension.Desugar.fsti
@@ -17,11 +17,11 @@
 module PulseSyntaxExtension.Desugar
 open FStarC
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 module Sugar = PulseSyntaxExtension.Sugar
 module SW = PulseSyntaxExtension.SyntaxWrapper
 module D = FStarC.Syntax.DsEnv
-module R = FStarC.Compiler.Range
+module R = FStarC.Range
 
 // An error can be "None", which means all relevant
 // errors were already logged via the error API.
diff --git a/src/syntax_extension/PulseSyntaxExtension.Env.fst b/src/syntax_extension/PulseSyntaxExtension.Env.fst
index 919cf2602..2585a8ff9 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Env.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.Env.fst
@@ -16,17 +16,17 @@
 
 module PulseSyntaxExtension.Env
 open FStarC
-open FStarC.Compiler.Effect
+open FStarC.Effect
 // module Sugar = PulseSugar
 module SW = PulseSyntaxExtension.SyntaxWrapper
 module A = FStarC.Parser.AST
 module D = FStarC.Syntax.DsEnv
 module S = FStarC.Syntax.Syntax
-module L = FStarC.Compiler.List
+module L = FStarC.List
 module U = FStarC.Syntax.Util
 module SS = FStarC.Syntax.Subst
-module R = FStarC.Compiler.Range
-module BU = FStarC.Compiler.Util
+module R = FStarC.Range
+module BU = FStarC.Util
 module P =  FStarC.Syntax.Print
 module ToSyntax = FStarC.ToSyntax.ToSyntax
 open FStarC.Class.Show
@@ -36,7 +36,7 @@ open FStarC.Ident
 open FStar.List.Tot
 open PulseSyntaxExtension.Err
 
-let r_ = FStarC.Compiler.Range.dummyRange
+let r_ = FStarC.Range.dummyRange
 #push-options "--warn_error -272" //intentional top-level effects
 let admit_lid = Ident.lid_of_path ["Prims"; "admit"] r_
 let pulse_lib_core_lid l = Ident.lid_of_path (["Pulse"; "Lib"; "Core"]@[l]) r_
diff --git a/src/syntax_extension/PulseSyntaxExtension.Err.fst b/src/syntax_extension/PulseSyntaxExtension.Err.fst
index e36efd6de..4b96504e9 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Err.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.Err.fst
@@ -16,8 +16,8 @@
 
 module PulseSyntaxExtension.Err
 open FStarC
-module R = FStarC.Compiler.Range
-open FStarC.Compiler.Effect
+module R = FStarC.Range
+open FStarC.Effect
 open FStarC.Class.HasRange
 open FStarC.Ident
 open FStarC.Class.Monad
@@ -74,7 +74,7 @@ let rec map2 (f : 'a -> 'b -> 'c) (xs : list 'a) (ys : list 'b) : err (list 'c)
     let! r = map2 f xx yy in
     return (f x y :: r)
   | _ ->
-    fail "map2: mismatch" FStarC.Compiler.Range.dummyRange
+    fail "map2: mismatch" FStarC.Range.dummyRange
 
 
 let left (f:either 'a 'b) (r:R.range)
diff --git a/src/syntax_extension/PulseSyntaxExtension.Parser.fsti b/src/syntax_extension/PulseSyntaxExtension.Parser.fsti
index 290e01ca1..5172306dd 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Parser.fsti
+++ b/src/syntax_extension/PulseSyntaxExtension.Parser.fsti
@@ -18,16 +18,16 @@ module PulseSyntaxExtension.Parser
 open FStarC
 
 val parse_peek_id (contents:string)
-                  (r:FStarC.Compiler.Range.range)
+                  (r:FStarC.Range.range)
   : either string
-           (string & FStarC.Compiler.Range.range)
+           (string & FStarC.Range.range)
 
 val parse_decl (contents:string)
-               (r:FStarC.Compiler.Range.range)
+               (r:FStarC.Range.range)
   : either PulseSyntaxExtension.Sugar.decl
-           (option (string & FStarC.Compiler.Range.range))
+           (option (string & FStarC.Range.range))
 
 val parse_lang (contents:string)
-               (r:FStarC.Compiler.Range.range)
+               (r:FStarC.Range.range)
   : either (list (either PulseSyntaxExtension.Sugar.decl FStarC.Parser.AST.decl) & option FStarC.Parser.ParseIt.parse_error)
-           (option (string & FStarC.Compiler.Range.range))
\ No newline at end of file
+           (option (string & FStarC.Range.range))
\ No newline at end of file
diff --git a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst
index 344878a80..a1a8a1d90 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst
@@ -22,8 +22,8 @@ module AU = FStarC.Parser.AST.Util
 open FStarC.Class.Show
 open FStarC.Class.Tagged
 
-let rng = FStarC.Compiler.Range.range
-let dummyRange = FStarC.Compiler.Range.dummyRange
+let rng = FStarC.Range.range
+let dummyRange = FStarC.Range.dummyRange
 
 //Note: We do not yet process binder attributes, like typeclass attributes
 type binder = A.binder
diff --git a/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti b/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti
index 2a8fd34ba..f0912c645 100644
--- a/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti
+++ b/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti
@@ -17,7 +17,7 @@
 module PulseSyntaxExtension.SyntaxWrapper
 open FStarC
 open FStarC.Ident
-let range = FStarC.Compiler.Range.range
+let range = FStarC.Range.range
 let var = nat
 let index = nat
 
diff --git a/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst b/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst
index 39f4df2cd..6d4d37152 100644
--- a/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst
+++ b/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst
@@ -16,17 +16,17 @@
 
 module PulseSyntaxExtension.TransformRValues
 open FStarC
-open FStarC.Compiler.Effect
+open FStarC.Effect
 module Sugar = PulseSyntaxExtension.Sugar
 module SW = PulseSyntaxExtension.SyntaxWrapper
 module A = FStarC.Parser.AST
 module D = FStarC.Syntax.DsEnv
 module S = FStarC.Syntax.Syntax
-module L = FStarC.Compiler.List
+module L = FStarC.List
 module U = FStarC.Syntax.Util
 module SS = FStarC.Syntax.Subst
-module R = FStarC.Compiler.Range
-module BU = FStarC.Compiler.Util
+module R = FStarC.Range
+module BU = FStarC.Util
 module P =  FStarC.Syntax.Print
 open FStarC.Class.Show
 open FStarC.Class.HasRange
@@ -266,7 +266,7 @@ let rec transform_stmt_with_reads (m:menv) (p:Sugar.stmt)
         | _ -> true in
 
       let! vs = pat_vars pat in
-      let m = Compiler.List.fold_left (fun m v -> menv_push_bv m v qualifier auto_deref_applicable) m vs in
+      let m = L.fold_left (fun m v -> menv_push_bv m v qualifier auto_deref_applicable) m vs in
 
       let p = { p with s=LetBinding { qualifier; pat; typ; init } } in
       return (p, needs, m)
diff --git a/src/syntax_extension/PulseSyntaxExtension.fst.config.json b/src/syntax_extension/PulseSyntaxExtension.fst.config.json
index 0c25a1a14..cdd1786cc 100644
--- a/src/syntax_extension/PulseSyntaxExtension.fst.config.json
+++ b/src/syntax_extension/PulseSyntaxExtension.fst.config.json
@@ -4,7 +4,7 @@
     "--query_cache",
     "--lax",
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--with_fstarc",
     "--z3version",
     "4.13.3",