diff --git a/Makefile.common b/Makefile.common
index 54495539c3..183f37f27d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -33,7 +33,13 @@ mustexist =						\
 $(call mustexist, FSTAR_EXE)
 $(call mustexist, KRML_HOME)
 
-FSTAR_ULIB := $(shell $(FSTAR_EXE) --locate_lib)
+# Note: fstar.exe --locate_lib returns the $PREFIX/lib/fstar directory,
+# which has ocaml files and much more. The fst/fstis are under a ulib/
+# subdirectory. There is an fstar.include in $PREFIX/lib/fstar to
+# include it, so most users do not need to know about ulib/, but we use
+# it explicitly in these Makefiles (and the vale-depend tool is not
+# aware of fstar.include).
+FSTAR_ULIB := $(shell $(FSTAR_EXE) --locate_lib)/ulib
 
 ifndef VALE_HOME
 # assuming an Everest source tree
@@ -60,10 +66,12 @@ VALE_HOME := $(call sanitize_path,$(VALE_HOME))
 
 include $(HACL_HOME)/Makefile.include
 
-# $(FSTAR_ULIB)/.cache necessary for Vale
+# $(FSTAR_ULIB)/.checked necessary for Vale. It must be the
+# directory where all of the checked files for the F* library can be
+# found (flat, no subdirs).
 INCLUDES = \
   $(ALL_HACL_DIRS) \
-  $(FSTAR_ULIB)/.cache \
+  $(FSTAR_ULIB)/.checked \
   $(KRML_HOME)/krmllib/obj \
   $(KRML_HOME)/krmllib
 
@@ -235,4 +243,4 @@ ALL_CMX_FILES = $(subst obj/Lib_Buffer.cmx,obj/Lib_Memzero0.cmx obj/Lib_Buffer.c
 # Warning 26: unused variable
 export OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs"
 OCAMLOPT = $(FSTAR_EXE) --ocamlenv ocamlfind opt -package fstar.lib -linkpkg -thread -g -I $(HACL_HOME)/obj -w -8-20-26
-OCAMLSHARED = $(FSTAR_EXE) --ocamlenv ocamlfind opt -shared -package fstar.lib -thread -g -I $(HACL_HOME)/obj -w -8-20-26
+OCAMLSHARED = $(FSTAR_EXE) --ocamlenv ocamlfind opt -shared -package fstar.pluginlib -thread -g -I $(HACL_HOME)/obj -w -8-20-26