diff --git a/src/fsdoc/generator.fs b/src/fsdoc/generator.fs
index 3881c825d9e..5c1d6fc8fe2 100644
--- a/src/fsdoc/generator.fs
+++ b/src/fsdoc/generator.fs
@@ -117,6 +117,7 @@ let string_of_decl' d =
   match d with 
   | TopLevelModule l -> "module " ^ l.str // SI: should never get here
   | Open l -> "open " ^ l.str
+  | Include l -> "include " ^ l.str
   | ModuleAbbrev (i, l) -> "module " ^ i.idText ^ " = " ^ l.str
   | KindAbbrev(i, _, _) -> "kind " ^ i.idText
   | TopLevelLet(_, _, pats) -> 
diff --git a/src/ocaml-output/FStar_Fsdoc_Generator.ml b/src/ocaml-output/FStar_Fsdoc_Generator.ml
index 767a195a6ac..91b5ad748fc 100755
--- a/src/ocaml-output/FStar_Fsdoc_Generator.ml
+++ b/src/ocaml-output/FStar_Fsdoc_Generator.ml
@@ -123,16 +123,19 @@ end
 | FStar_Parser_AST.Open (l) -> begin
 (Prims.strcat "open " l.FStar_Ident.str)
 end
+| FStar_Parser_AST.Include (l) -> begin
+(Prims.strcat "include " l.FStar_Ident.str)
+end
 | FStar_Parser_AST.ModuleAbbrev (i, l) -> begin
 (Prims.strcat "module " (Prims.strcat i.FStar_Ident.idText (Prims.strcat " = " l.FStar_Ident.str)))
 end
-| FStar_Parser_AST.KindAbbrev (i, _82_71, _82_73) -> begin
+| FStar_Parser_AST.KindAbbrev (i, _82_73, _82_75) -> begin
 (Prims.strcat "kind " i.FStar_Ident.idText)
 end
-| FStar_Parser_AST.TopLevelLet (_82_77, _82_79, pats) -> begin
+| FStar_Parser_AST.TopLevelLet (_82_79, _82_81, pats) -> begin
 (
 
-let termty = (FStar_List.map (fun _82_85 -> (match (_82_85) with
+let termty = (FStar_List.map (fun _82_87 -> (match (_82_87) with
 | (p, t) -> begin
 (let _177_70 = (FStar_Parser_AST.pat_to_string p)
 in (let _177_69 = (FStar_Parser_AST.term_to_string t)
@@ -140,23 +143,23 @@ in ((_177_70), (_177_69))))
 end)) pats)
 in (
 
-let termty' = (FStar_List.map (fun _82_89 -> (match (_82_89) with
+let termty' = (FStar_List.map (fun _82_91 -> (match (_82_91) with
 | (p, t) -> begin
 (Prims.strcat p (Prims.strcat ":" t))
 end)) termty)
 in (Prims.strcat "let " (FStar_String.concat ", " termty'))))
 end
-| FStar_Parser_AST.Main (_82_92) -> begin
+| FStar_Parser_AST.Main (_82_94) -> begin
 "main ..."
 end
-| FStar_Parser_AST.Assume (_82_95, i, t) -> begin
+| FStar_Parser_AST.Assume (_82_97, i, t) -> begin
 (let _177_74 = (let _177_73 = (let _177_72 = (FStar_Parser_AST.term_to_string t)
 in (Prims.strcat ":" _177_72))
 in (Prims.strcat i.FStar_Ident.idText _177_73))
 in (Prims.strcat "assume " _177_74))
 end
-| FStar_Parser_AST.Tycon (_82_101, tys) -> begin
-(let _177_80 = (let _177_79 = (FStar_All.pipe_right tys (FStar_List.map (fun _82_107 -> (match (_82_107) with
+| FStar_Parser_AST.Tycon (_82_103, tys) -> begin
+(let _177_80 = (let _177_79 = (FStar_All.pipe_right tys (FStar_List.map (fun _82_109 -> (match (_82_109) with
 | (t, d) -> begin
 (let _177_78 = (string_of_tycon t)
 in (let _177_77 = (let _177_76 = (string_of_fsdoco d)
@@ -166,13 +169,13 @@ end))))
 in (FStar_All.pipe_right _177_79 (FStar_String.concat " and ")))
 in (Prims.strcat "type " _177_80))
 end
-| FStar_Parser_AST.Val (_82_109, i, t) -> begin
+| FStar_Parser_AST.Val (_82_111, i, t) -> begin
 (let _177_83 = (let _177_82 = (let _177_81 = (FStar_Parser_AST.term_to_string t)
 in (Prims.strcat ":" _177_81))
 in (Prims.strcat i.FStar_Ident.idText _177_82))
 in (Prims.strcat "val " _177_83))
 end
-| FStar_Parser_AST.Exception (i, _82_116) -> begin
+| FStar_Parser_AST.Exception (i, _82_118) -> begin
 (Prims.strcat "exception " i.FStar_Ident.idText)
 end
 | (FStar_Parser_AST.NewEffect (_, FStar_Parser_AST.DefineEffect (i, _, _, _, _))) | (FStar_Parser_AST.NewEffect (_, FStar_Parser_AST.RedefineEffect (i, _, _))) -> begin
@@ -181,13 +184,13 @@ end
 | (FStar_Parser_AST.NewEffectForFree (_, FStar_Parser_AST.DefineEffect (i, _, _, _, _))) | (FStar_Parser_AST.NewEffectForFree (_, FStar_Parser_AST.RedefineEffect (i, _, _))) -> begin
 (Prims.strcat "new_effect_for_free " i.FStar_Ident.idText)
 end
-| FStar_Parser_AST.SubEffect (_82_170) -> begin
+| FStar_Parser_AST.SubEffect (_82_172) -> begin
 "sub_effect"
 end
-| FStar_Parser_AST.Pragma (_82_173) -> begin
+| FStar_Parser_AST.Pragma (_82_175) -> begin
 "pragma"
 end
-| FStar_Parser_AST.Fsdoc (comm, _82_177) -> begin
+| FStar_Parser_AST.Fsdoc (comm, _82_179) -> begin
 comm
 end))
 
@@ -200,35 +203,35 @@ let tyconvars_documented = (fun tycon -> (match (tycon) with
 | (FStar_Parser_AST.TyconAbstract (_)) | (FStar_Parser_AST.TyconAbbrev (_)) -> begin
 false
 end
-| FStar_Parser_AST.TyconRecord (_82_192, _82_194, _82_196, fields) -> begin
-(FStar_List.existsb (fun _82_203 -> (match (_82_203) with
+| FStar_Parser_AST.TyconRecord (_82_194, _82_196, _82_198, fields) -> begin
+(FStar_List.existsb (fun _82_205 -> (match (_82_205) with
 | (_id, _t, doco) -> begin
 (FStar_Util.is_some doco)
 end)) fields)
 end
-| FStar_Parser_AST.TyconVariant (_82_205, _82_207, _82_209, vars) -> begin
-(FStar_List.existsb (fun _82_217 -> (match (_82_217) with
+| FStar_Parser_AST.TyconVariant (_82_207, _82_209, _82_211, vars) -> begin
+(FStar_List.existsb (fun _82_219 -> (match (_82_219) with
 | (_id, _t, doco, _u) -> begin
 (FStar_Util.is_some doco)
 end)) vars)
 end))
-in (FStar_List.existsb (fun _82_220 -> (match (_82_220) with
+in (FStar_List.existsb (fun _82_222 -> (match (_82_222) with
 | (tycon, doco) -> begin
 ((tyconvars_documented tycon) || (FStar_Util.is_some doco))
 end)) tt)))
 in (match (d.FStar_Parser_AST.doc) with
-| Some (_82_222) -> begin
+| Some (_82_224) -> begin
 true
 end
-| _82_225 -> begin
+| _82_227 -> begin
 (match (d.FStar_Parser_AST.d) with
-| FStar_Parser_AST.Fsdoc (_82_227) -> begin
+| FStar_Parser_AST.Fsdoc (_82_229) -> begin
 true
 end
-| FStar_Parser_AST.Tycon (_82_230, ty) -> begin
+| FStar_Parser_AST.Tycon (_82_232, ty) -> begin
 (tycon_documented ty)
 end
-| _82_235 -> begin
+| _82_237 -> begin
 false
 end)
 end)))
@@ -237,21 +240,21 @@ end)))
 let document_decl : (Prims.string  ->  Prims.unit)  ->  FStar_Parser_AST.decl  ->  Prims.unit = (fun w d -> if (decl_documented d) then begin
 (
 
-let _82_242 = d
-in (match (_82_242) with
-| {FStar_Parser_AST.d = decl; FStar_Parser_AST.drange = _82_240; FStar_Parser_AST.doc = fsdoc} -> begin
+let _82_244 = d
+in (match (_82_244) with
+| {FStar_Parser_AST.d = decl; FStar_Parser_AST.drange = _82_242; FStar_Parser_AST.doc = fsdoc} -> begin
 (
 
-let _82_243 = (let _177_103 = (let _177_102 = (string_of_decl' d.FStar_Parser_AST.d)
+let _82_245 = (let _177_103 = (let _177_102 = (string_of_decl' d.FStar_Parser_AST.d)
 in (code_wrap _177_102))
 in (w _177_103))
 in (
 
-let _82_251 = (match (fsdoc) with
+let _82_253 = (match (fsdoc) with
 | Some (doc, _kw) -> begin
 (w (Prims.strcat "\n" doc))
 end
-| _82_250 -> begin
+| _82_252 -> begin
 ()
 end)
 in (w "")))
@@ -262,17 +265,17 @@ end)
 
 
 let document_toplevel = (fun name topdecl -> (match (topdecl.FStar_Parser_AST.d) with
-| FStar_Parser_AST.TopLevelModule (_82_256) -> begin
+| FStar_Parser_AST.TopLevelModule (_82_258) -> begin
 (match (topdecl.FStar_Parser_AST.doc) with
 | Some (doc, kw) -> begin
-(match ((FStar_List.tryFind (fun _82_264 -> (match (_82_264) with
+(match ((FStar_List.tryFind (fun _82_266 -> (match (_82_266) with
 | (k, v) -> begin
 (k = "summary")
 end)) kw)) with
 | None -> begin
 ((None), (Some (doc)))
 end
-| Some (_82_267, summary) -> begin
+| Some (_82_269, summary) -> begin
 ((Some (summary)), (Some (doc)))
 end)
 end
@@ -280,21 +283,21 @@ end
 ((None), (None))
 end)
 end
-| _82_273 -> begin
+| _82_275 -> begin
 (Prims.raise (FStar_Syntax_Syntax.Err ("Not a TopLevelModule")))
 end))
 
 
 let document_module : FStar_Parser_AST.modul  ->  FStar_Ident.lid = (fun m -> (
 
-let _82_288 = (match (m) with
+let _82_290 = (match (m) with
 | FStar_Parser_AST.Module (n, d) -> begin
 ((n), (d), ("module"))
 end
-| FStar_Parser_AST.Interface (n, d, _82_282) -> begin
+| FStar_Parser_AST.Interface (n, d, _82_284) -> begin
 ((n), (d), ("interface"))
 end)
-in (match (_82_288) with
+in (match (_82_290) with
 | (name, decls, _mt) -> begin
 (match ((one_toplevel decls)) with
 | Some (top_decl, other_decls) -> begin
@@ -315,8 +318,8 @@ in (
 let no_comment = "fsdoc: no-comment-found"
 in (
 
-let _82_300 = (document_toplevel name top_decl)
-in (match (_82_300) with
+let _82_302 = (document_toplevel name top_decl)
+in (match (_82_302) with
 | (summary, comment) -> begin
 (
 
@@ -338,22 +341,22 @@ no_comment
 end)
 in (
 
-let _82_309 = (let _177_110 = (FStar_Util.format "# module %s" ((name.FStar_Ident.str)::[]))
+let _82_311 = (let _177_110 = (FStar_Util.format "# module %s" ((name.FStar_Ident.str)::[]))
 in (w _177_110))
 in (
 
-let _82_311 = (let _177_111 = (FStar_Util.format "%s\n" ((summary)::[]))
+let _82_313 = (let _177_111 = (FStar_Util.format "%s\n" ((summary)::[]))
 in (w _177_111))
 in (
 
-let _82_313 = (let _177_112 = (FStar_Util.format "%s\n" ((comment)::[]))
+let _82_315 = (let _177_112 = (FStar_Util.format "%s\n" ((comment)::[]))
 in (w _177_112))
 in (
 
-let _82_315 = (FStar_List.iter (document_decl w) other_decls)
+let _82_317 = (FStar_List.iter (document_decl w) other_decls)
 in (
 
-let _82_317 = (FStar_Util.close_file fd)
+let _82_319 = (FStar_Util.close_file fd)
 in name)))))))
 end)))))))
 end
@@ -379,7 +382,7 @@ in (
 let fd = (FStar_Util.open_file_for_writing on)
 in (
 
-let _82_327 = (FStar_List.iter (fun m -> (let _177_119 = (FStar_Util.format "%s\n" ((m.FStar_Ident.str)::[]))
+let _82_329 = (FStar_List.iter (fun m -> (let _177_119 = (FStar_Util.format "%s\n" ((m.FStar_Ident.str)::[]))
 in (FStar_Util.append_to_file fd _177_119))) mods)
 in (FStar_Util.close_file fd)))))))
 
diff --git a/src/ocaml-output/FStar_Parser_AST.ml b/src/ocaml-output/FStar_Parser_AST.ml
index de6026e4245..01c4c5dbc47 100755
--- a/src/ocaml-output/FStar_Parser_AST.ml
+++ b/src/ocaml-output/FStar_Parser_AST.ml
@@ -1301,6 +1301,7 @@ end))
 type decl' =
 | TopLevelModule of FStar_Ident.lid
 | Open of FStar_Ident.lid
+| Include of FStar_Ident.lid
 | ModuleAbbrev of (FStar_Ident.ident * FStar_Ident.lid)
 | KindAbbrev of (FStar_Ident.ident * binder Prims.list * knd)
 | TopLevelLet of (qualifiers * let_qualifier * (pattern * term) Prims.list)
@@ -1339,6 +1340,15 @@ false
 end))
 
 
+let is_Include = (fun _discr_ -> (match (_discr_) with
+| Include (_) -> begin
+true
+end
+| _ -> begin
+false
+end))
+
+
 let is_ModuleAbbrev = (fun _discr_ -> (match (_discr_) with
 | ModuleAbbrev (_) -> begin
 true
@@ -1489,93 +1499,99 @@ _60_194
 end))
 
 
-let ___ModuleAbbrev____0 = (fun projectee -> (match (projectee) with
-| ModuleAbbrev (_60_197) -> begin
+let ___Include____0 = (fun projectee -> (match (projectee) with
+| Include (_60_197) -> begin
 _60_197
 end))
 
 
-let ___KindAbbrev____0 = (fun projectee -> (match (projectee) with
-| KindAbbrev (_60_200) -> begin
+let ___ModuleAbbrev____0 = (fun projectee -> (match (projectee) with
+| ModuleAbbrev (_60_200) -> begin
 _60_200
 end))
 
 
-let ___TopLevelLet____0 = (fun projectee -> (match (projectee) with
-| TopLevelLet (_60_203) -> begin
+let ___KindAbbrev____0 = (fun projectee -> (match (projectee) with
+| KindAbbrev (_60_203) -> begin
 _60_203
 end))
 
 
-let ___Main____0 = (fun projectee -> (match (projectee) with
-| Main (_60_206) -> begin
+let ___TopLevelLet____0 = (fun projectee -> (match (projectee) with
+| TopLevelLet (_60_206) -> begin
 _60_206
 end))
 
 
-let ___Assume____0 = (fun projectee -> (match (projectee) with
-| Assume (_60_209) -> begin
+let ___Main____0 = (fun projectee -> (match (projectee) with
+| Main (_60_209) -> begin
 _60_209
 end))
 
 
-let ___Tycon____0 = (fun projectee -> (match (projectee) with
-| Tycon (_60_212) -> begin
+let ___Assume____0 = (fun projectee -> (match (projectee) with
+| Assume (_60_212) -> begin
 _60_212
 end))
 
 
-let ___Val____0 = (fun projectee -> (match (projectee) with
-| Val (_60_215) -> begin
+let ___Tycon____0 = (fun projectee -> (match (projectee) with
+| Tycon (_60_215) -> begin
 _60_215
 end))
 
 
-let ___Exception____0 = (fun projectee -> (match (projectee) with
-| Exception (_60_218) -> begin
+let ___Val____0 = (fun projectee -> (match (projectee) with
+| Val (_60_218) -> begin
 _60_218
 end))
 
 
-let ___NewEffect____0 = (fun projectee -> (match (projectee) with
-| NewEffect (_60_221) -> begin
+let ___Exception____0 = (fun projectee -> (match (projectee) with
+| Exception (_60_221) -> begin
 _60_221
 end))
 
 
-let ___NewEffectForFree____0 = (fun projectee -> (match (projectee) with
-| NewEffectForFree (_60_224) -> begin
+let ___NewEffect____0 = (fun projectee -> (match (projectee) with
+| NewEffect (_60_224) -> begin
 _60_224
 end))
 
 
-let ___SubEffect____0 = (fun projectee -> (match (projectee) with
-| SubEffect (_60_227) -> begin
+let ___NewEffectForFree____0 = (fun projectee -> (match (projectee) with
+| NewEffectForFree (_60_227) -> begin
 _60_227
 end))
 
 
-let ___Pragma____0 = (fun projectee -> (match (projectee) with
-| Pragma (_60_230) -> begin
+let ___SubEffect____0 = (fun projectee -> (match (projectee) with
+| SubEffect (_60_230) -> begin
 _60_230
 end))
 
 
-let ___Fsdoc____0 = (fun projectee -> (match (projectee) with
-| Fsdoc (_60_233) -> begin
+let ___Pragma____0 = (fun projectee -> (match (projectee) with
+| Pragma (_60_233) -> begin
 _60_233
 end))
 
 
+let ___Fsdoc____0 = (fun projectee -> (match (projectee) with
+| Fsdoc (_60_236) -> begin
+_60_236
+end))
+
+
 let ___DefineEffect____0 = (fun projectee -> (match (projectee) with
-| DefineEffect (_60_237) -> begin
-_60_237
+| DefineEffect (_60_240) -> begin
+_60_240
 end))
 
 
 let ___RedefineEffect____0 = (fun projectee -> (match (projectee) with
-| RedefineEffect (_60_240) -> begin
-_60_240
+| RedefineEffect (_60_243) -> begin
+_60_243
 end))
 
 
@@ -1603,14 +1619,14 @@ end))
 
 
 let ___Module____0 = (fun projectee -> (match (projectee) with
-| Module (_60_243) -> begin
-_60_243
+| Module (_60_246) -> begin
+_60_246
 end))
 
 
 let ___Interface____0 = (fun projectee -> (match (projectee) with
-| Interface (_60_246) -> begin
-_60_246
+| Interface (_60_249) -> begin
+_60_249
 end))
 
 
@@ -1629,10 +1645,10 @@ let first_char = (FStar_String.substring id.FStar_Ident.idText (Prims.parse_int
 in if ((FStar_String.lowercase first_char) = first_char) then begin
 ()
 end else begin
-(let _155_1125 = (let _155_1124 = (let _155_1123 = (FStar_Util.format1 "Invalid identifer \'%s\'; expected a symbol that begins with a lower-case character" id.FStar_Ident.idText)
-in ((_155_1123), (id.FStar_Ident.idRange)))
-in FStar_Syntax_Syntax.Error (_155_1124))
-in (Prims.raise _155_1125))
+(let _155_1139 = (let _155_1138 = (let _155_1137 = (FStar_Util.format1 "Invalid identifer \'%s\'; expected a symbol that begins with a lower-case character" id.FStar_Ident.idText)
+in ((_155_1137), (id.FStar_Ident.idRange)))
+in FStar_Syntax_Syntax.Error (_155_1138))
+in (Prims.raise _155_1139))
 end)
 end else begin
 ()
@@ -1654,7 +1670,7 @@ let t = (match (t.tm) with
 | Const (FStar_Const.Const_int (s, Some (FStar_Const.Signed, width))) -> begin
 Const (FStar_Const.Const_int ((((Prims.strcat "-" s)), (Some (((FStar_Const.Signed), (width)))))))
 end
-| _60_271 -> begin
+| _60_274 -> begin
 Op ((("-"), ((t)::[])))
 end)
 in (mk_term t r l)))
@@ -1667,7 +1683,7 @@ let un_curry_abs : pattern Prims.list  ->  term  ->  term' = (fun ps body -> (ma
 | Abs (p', body') -> begin
 Abs ((((FStar_List.append ps p')), (body')))
 end
-| _60_282 -> begin
+| _60_285 -> begin
 Abs (((ps), (body)))
 end))
 
@@ -1682,28 +1698,28 @@ in (FStar_Ident.gen r1))
 end else begin
 (FStar_Absyn_Util.genident (Some (r1)))
 end
-in (let _155_1173 = (let _155_1172 = (let _155_1171 = (let _155_1170 = (let _155_1169 = (let _155_1168 = (let _155_1167 = (let _155_1166 = (FStar_Ident.lid_of_ids ((x)::[]))
-in Var (_155_1166))
-in (mk_term _155_1167 r1 Expr))
-in ((_155_1168), (branches)))
-in Match (_155_1169))
-in (mk_term _155_1170 r2 Expr))
-in ((((mk_pattern (PatVar (((x), (None)))) r1))::[]), (_155_1171)))
-in Abs (_155_1172))
-in (mk_term _155_1173 r2 Expr))))
+in (let _155_1187 = (let _155_1186 = (let _155_1185 = (let _155_1184 = (let _155_1183 = (let _155_1182 = (let _155_1181 = (let _155_1180 = (FStar_Ident.lid_of_ids ((x)::[]))
+in Var (_155_1180))
+in (mk_term _155_1181 r1 Expr))
+in ((_155_1182), (branches)))
+in Match (_155_1183))
+in (mk_term _155_1184 r2 Expr))
+in ((((mk_pattern (PatVar (((x), (None)))) r1))::[]), (_155_1185)))
+in Abs (_155_1186))
+in (mk_term _155_1187 r2 Expr))))
 
 
 let un_function : pattern  ->  term  ->  (pattern * term) Prims.option = (fun p tm -> (match (((p.pat), (tm.tm))) with
-| (PatVar (_60_291), Abs (pats, body)) -> begin
+| (PatVar (_60_294), Abs (pats, body)) -> begin
 Some ((((mk_pattern (PatApp (((p), (pats)))) p.prange)), (body)))
 end
-| _60_299 -> begin
+| _60_302 -> begin
 None
 end))
 
 
-let lid_with_range : FStar_Ident.lident  ->  FStar_Range.range  ->  FStar_Ident.lident = (fun lid r -> (let _155_1182 = (FStar_Ident.path_of_lid lid)
-in (FStar_Ident.lid_of_path _155_1182 r)))
+let lid_with_range : FStar_Ident.lident  ->  FStar_Range.range  ->  FStar_Ident.lident = (fun lid r -> (let _155_1196 = (FStar_Ident.path_of_lid lid)
+in (FStar_Ident.lid_of_path _155_1196 r)))
 
 
 let consPat : FStar_Range.range  ->  pattern  ->  pattern  ->  pattern' = (fun r hd tl -> PatApp ((((mk_pattern (PatName (FStar_Absyn_Const.cons_lid)) r)), ((hd)::(tl)::[]))))
@@ -1731,13 +1747,13 @@ let mkApp : term  ->  (term * imp) Prims.list  ->  FStar_Range.range  ->  term =
 | [] -> begin
 t
 end
-| _60_326 -> begin
+| _60_329 -> begin
 (match (t.tm) with
 | Name (s) -> begin
 (mk_term (Construct (((s), (args)))) r Un)
 end
-| _60_330 -> begin
-(FStar_List.fold_left (fun t _60_334 -> (match (_60_334) with
+| _60_333 -> begin
+(FStar_List.fold_left (fun t _60_337 -> (match (_60_337) with
 | (a, imp) -> begin
 (mk_term (App (((t), (a), (imp)))) r Un)
 end)) t args)
@@ -1750,12 +1766,12 @@ let mkRefSet : FStar_Range.range  ->  term Prims.list  ->  term = (fun r elts ->
 let univs = (FStar_Options.universes ())
 in (
 
-let _60_341 = if univs then begin
+let _60_344 = if univs then begin
 ((FStar_Absyn_Const.tset_empty), (FStar_Absyn_Const.tset_singleton), (FStar_Absyn_Const.tset_union))
 end else begin
 ((FStar_Absyn_Const.set_empty), (FStar_Absyn_Const.set_singleton), (FStar_Absyn_Const.set_union))
 end
-in (match (_60_341) with
+in (match (_60_344) with
 | (empty_lid, singleton_lid, union_lid) -> begin
 (
 
@@ -1783,15 +1799,15 @@ let mkExplicitApp : term  ->  term Prims.list  ->  FStar_Range.range  ->  term =
 | [] -> begin
 t
 end
-| _60_355 -> begin
+| _60_358 -> begin
 (match (t.tm) with
 | Name (s) -> begin
-(let _155_1236 = (let _155_1235 = (let _155_1234 = (FStar_List.map (fun a -> ((a), (Nothing))) args)
-in ((s), (_155_1234)))
-in Construct (_155_1235))
-in (mk_term _155_1236 r Un))
+(let _155_1250 = (let _155_1249 = (let _155_1248 = (FStar_List.map (fun a -> ((a), (Nothing))) args)
+in ((s), (_155_1248)))
+in Construct (_155_1249))
+in (mk_term _155_1250 r Un))
 end
-| _60_360 -> begin
+| _60_363 -> begin
 (FStar_List.fold_left (fun t a -> (mk_term (App (((t), (a), (Nothing)))) r Un)) t args)
 end)
 end))
@@ -1818,8 +1834,8 @@ let admit_magic = (mk_term (Seq (((admit), (magic)))) r Expr)
 in admit_magic)))))
 
 
-let mkWildAdmitMagic = (fun r -> (let _155_1242 = (mkAdmitMagic r)
-in (((mk_pattern PatWild r)), (None), (_155_1242))))
+let mkWildAdmitMagic = (fun r -> (let _155_1256 = (mkAdmitMagic r)
+in (((mk_pattern PatWild r)), (None), (_155_1256))))
 
 
 let focusBranches = (fun branches r -> (
@@ -1828,14 +1844,14 @@ let should_filter = (FStar_Util.for_some Prims.fst branches)
 in if should_filter then begin
 (
 
-let _60_374 = (FStar_Tc_Errors.warn r "Focusing on only some cases")
+let _60_377 = (FStar_Tc_Errors.warn r "Focusing on only some cases")
 in (
 
-let focussed = (let _155_1245 = (FStar_List.filter Prims.fst branches)
-in (FStar_All.pipe_right _155_1245 (FStar_List.map Prims.snd)))
-in (let _155_1247 = (let _155_1246 = (mkWildAdmitMagic r)
-in (_155_1246)::[])
-in (FStar_List.append focussed _155_1247))))
+let focussed = (let _155_1259 = (FStar_List.filter Prims.fst branches)
+in (FStar_All.pipe_right _155_1259 (FStar_List.map Prims.snd)))
+in (let _155_1261 = (let _155_1260 = (mkWildAdmitMagic r)
+in (_155_1260)::[])
+in (FStar_List.append focussed _155_1261))))
 end else begin
 (FStar_All.pipe_right branches (FStar_List.map Prims.snd))
 end))
@@ -1847,14 +1863,14 @@ let should_filter = (FStar_Util.for_some Prims.fst lbs)
 in if should_filter then begin
 (
 
-let _60_380 = (FStar_Tc_Errors.warn r "Focusing on only some cases in this (mutually) recursive definition")
-in (FStar_List.map (fun _60_384 -> (match (_60_384) with
+let _60_383 = (FStar_Tc_Errors.warn r "Focusing on only some cases in this (mutually) recursive definition")
+in (FStar_List.map (fun _60_387 -> (match (_60_387) with
 | (f, lb) -> begin
 if f then begin
 lb
 end else begin
-(let _155_1251 = (mkAdmitMagic r)
-in (((Prims.fst lb)), (_155_1251)))
+(let _155_1265 = (mkAdmitMagic r)
+in (((Prims.fst lb)), (_155_1265)))
 end
 end)) lbs))
 end else begin
@@ -1862,8 +1878,8 @@ end else begin
 end))
 
 
-let mkFsTypApp : term  ->  term Prims.list  ->  FStar_Range.range  ->  term = (fun t args r -> (let _155_1259 = (FStar_List.map (fun a -> ((a), (FsTypApp))) args)
-in (mkApp t _155_1259 r)))
+let mkFsTypApp : term  ->  term Prims.list  ->  FStar_Range.range  ->  term = (fun t args r -> (let _155_1273 = (FStar_List.map (fun a -> ((a), (FsTypApp))) args)
+in (mkApp t _155_1273 r)))
 
 
 let mkTuple : term Prims.list  ->  FStar_Range.range  ->  term = (fun args r -> (
@@ -1873,8 +1889,8 @@ let cons = if (FStar_Options.universes ()) then begin
 end else begin
 (FStar_Absyn_Util.mk_tuple_data_lid (FStar_List.length args) r)
 end
-in (let _155_1265 = (FStar_List.map (fun x -> ((x), (Nothing))) args)
-in (mkApp (mk_term (Name (cons)) r Expr) _155_1265 r))))
+in (let _155_1279 = (FStar_List.map (fun x -> ((x), (Nothing))) args)
+in (mkApp (mk_term (Name (cons)) r Expr) _155_1279 r))))
 
 
 let mkDTuple : term Prims.list  ->  FStar_Range.range  ->  term = (fun args r -> (
@@ -1884,8 +1900,8 @@ let cons = if (FStar_Options.universes ()) then begin
 end else begin
 (FStar_Absyn_Util.mk_dtuple_data_lid (FStar_List.length args) r)
 end
-in (let _155_1271 = (FStar_List.map (fun x -> ((x), (Nothing))) args)
-in (mkApp (mk_term (Name (cons)) r Expr) _155_1271 r))))
+in (let _155_1285 = (FStar_List.map (fun x -> ((x), (Nothing))) args)
+in (mkApp (mk_term (Name (cons)) r Expr) _155_1285 r))))
 
 
 let mkRefinedBinder : FStar_Ident.ident  ->  term  ->  Prims.bool  ->  term Prims.option  ->  FStar_Range.range  ->  aqual  ->  binder = (fun id t should_bind_var refopt m implicit -> (
@@ -1916,10 +1932,10 @@ end
 | Some (phi) -> begin
 if should_bind_pat then begin
 (match (pat.pat) with
-| PatVar (x, _60_419) -> begin
+| PatVar (x, _60_422) -> begin
 (mk_term (Refine ((((mk_binder (Annotated (((x), (t)))) t_range Type None)), (phi)))) range Type)
 end
-| _60_423 -> begin
+| _60_426 -> begin
 (
 
 let x = (FStar_Ident.gen t_range)
@@ -1927,18 +1943,18 @@ in (
 
 let phi = (
 
-let x_var = (let _155_1297 = (let _155_1296 = (FStar_Ident.lid_of_ids ((x)::[]))
-in Var (_155_1296))
-in (mk_term _155_1297 phi.range Formula))
+let x_var = (let _155_1311 = (let _155_1310 = (FStar_Ident.lid_of_ids ((x)::[]))
+in Var (_155_1310))
+in (mk_term _155_1311 phi.range Formula))
 in (
 
 let pat_branch = ((pat), (None), (phi))
 in (
 
-let otherwise_branch = (let _155_1300 = (let _155_1299 = (let _155_1298 = (FStar_Ident.lid_of_path (("False")::[]) phi.range)
-in Name (_155_1298))
-in (mk_term _155_1299 phi.range Formula))
-in (((mk_pattern PatWild phi.range)), (None), (_155_1300)))
+let otherwise_branch = (let _155_1314 = (let _155_1313 = (let _155_1312 = (FStar_Ident.lid_of_path (("False")::[]) phi.range)
+in Name (_155_1312))
+in (mk_term _155_1313 phi.range Formula))
+in (((mk_pattern PatWild phi.range)), (None), (_155_1314)))
 in (mk_term (Match (((x_var), ((pat_branch)::(otherwise_branch)::[])))) phi.range Formula))))
 in (mk_term (Refine ((((mk_binder (Annotated (((x), (t)))) t_range Type None)), (phi)))) range Type)))
 end)
@@ -1953,25 +1969,25 @@ let rec extract_named_refinement : term  ->  (FStar_Ident.ident * term * term Pr
 | NamedTyp (x, t) -> begin
 Some (((x), (t), (None)))
 end
-| Refine ({b = Annotated (x, t); brange = _60_440; blevel = _60_438; aqual = _60_436}, t') -> begin
+| Refine ({b = Annotated (x, t); brange = _60_443; blevel = _60_441; aqual = _60_439}, t') -> begin
 Some (((x), (t), (Some (t'))))
 end
 | Paren (t) -> begin
 (extract_named_refinement t)
 end
-| _60_452 -> begin
+| _60_455 -> begin
 None
 end))
 
 
-let string_of_fsdoc : (Prims.string * (Prims.string * Prims.string) Prims.list)  ->  Prims.string = (fun _60_455 -> (match (_60_455) with
+let string_of_fsdoc : (Prims.string * (Prims.string * Prims.string) Prims.list)  ->  Prims.string = (fun _60_458 -> (match (_60_458) with
 | (comment, keywords) -> begin
-(let _155_1307 = (let _155_1306 = (FStar_List.map (fun _60_458 -> (match (_60_458) with
+(let _155_1321 = (let _155_1320 = (FStar_List.map (fun _60_461 -> (match (_60_461) with
 | (k, v) -> begin
 (Prims.strcat k (Prims.strcat "->" v))
 end)) keywords)
-in (FStar_String.concat "," _155_1306))
-in (Prims.strcat comment _155_1307))
+in (FStar_String.concat "," _155_1320))
+in (Prims.strcat comment _155_1321))
 end))
 
 
@@ -1987,15 +2003,15 @@ end
 end))
 
 
-let to_string_l = (fun sep f l -> (let _155_1316 = (FStar_List.map f l)
-in (FStar_String.concat sep _155_1316)))
+let to_string_l = (fun sep f l -> (let _155_1330 = (FStar_List.map f l)
+in (FStar_String.concat sep _155_1330)))
 
 
 let imp_to_string : imp  ->  Prims.string = (fun _60_2 -> (match (_60_2) with
 | Hash -> begin
 "#"
 end
-| _60_469 -> begin
+| _60_472 -> begin
 ""
 end))
 
@@ -2004,25 +2020,25 @@ let rec term_to_string : term  ->  Prims.string = (fun x -> (match (x.tm) with
 | Wild -> begin
 "_"
 end
-| Requires (t, _60_474) -> begin
-(let _155_1324 = (term_to_string t)
-in (FStar_Util.format1 "(requires %s)" _155_1324))
+| Requires (t, _60_477) -> begin
+(let _155_1338 = (term_to_string t)
+in (FStar_Util.format1 "(requires %s)" _155_1338))
 end
-| Ensures (t, _60_479) -> begin
-(let _155_1325 = (term_to_string t)
-in (FStar_Util.format1 "(ensures %s)" _155_1325))
+| Ensures (t, _60_482) -> begin
+(let _155_1339 = (term_to_string t)
+in (FStar_Util.format1 "(ensures %s)" _155_1339))
 end
-| Labeled (t, l, _60_485) -> begin
-(let _155_1326 = (term_to_string t)
-in (FStar_Util.format2 "(labeled %s %s)" l _155_1326))
+| Labeled (t, l, _60_488) -> begin
+(let _155_1340 = (term_to_string t)
+in (FStar_Util.format2 "(labeled %s %s)" l _155_1340))
 end
 | Const (c) -> begin
 (FStar_Absyn_Print.const_to_string c)
 end
 | Op (s, xs) -> begin
-(let _155_1329 = (let _155_1328 = (FStar_List.map (fun x -> (FStar_All.pipe_right x term_to_string)) xs)
-in (FStar_String.concat ", " _155_1328))
-in (FStar_Util.format2 "%s(%s)" s _155_1329))
+(let _155_1343 = (let _155_1342 = (FStar_List.map (fun x -> (FStar_All.pipe_right x term_to_string)) xs)
+in (FStar_String.concat ", " _155_1342))
+in (FStar_Util.format2 "%s(%s)" s _155_1343))
 end
 | Tvar (id) -> begin
 id.FStar_Ident.idText
@@ -2031,93 +2047,93 @@ end
 l.FStar_Ident.str
 end
 | Construct (l, args) -> begin
-(let _155_1332 = (to_string_l " " (fun _60_506 -> (match (_60_506) with
+(let _155_1346 = (to_string_l " " (fun _60_509 -> (match (_60_509) with
 | (a, imp) -> begin
-(let _155_1331 = (term_to_string a)
-in (FStar_Util.format2 "%s%s" (imp_to_string imp) _155_1331))
+(let _155_1345 = (term_to_string a)
+in (FStar_Util.format2 "%s%s" (imp_to_string imp) _155_1345))
 end)) args)
-in (FStar_Util.format2 "(%s %s)" l.FStar_Ident.str _155_1332))
+in (FStar_Util.format2 "(%s %s)" l.FStar_Ident.str _155_1346))
 end
 | Abs (pats, t) -> begin
-(let _155_1334 = (to_string_l " " pat_to_string pats)
-in (let _155_1333 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "(fun %s -> %s)" _155_1334 _155_1333)))
+(let _155_1348 = (to_string_l " " pat_to_string pats)
+in (let _155_1347 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "(fun %s -> %s)" _155_1348 _155_1347)))
 end
 | App (t1, t2, imp) -> begin
-(let _155_1336 = (FStar_All.pipe_right t1 term_to_string)
-in (let _155_1335 = (FStar_All.pipe_right t2 term_to_string)
-in (FStar_Util.format3 "%s %s%s" _155_1336 (imp_to_string imp) _155_1335)))
+(let _155_1350 = (FStar_All.pipe_right t1 term_to_string)
+in (let _155_1349 = (FStar_All.pipe_right t2 term_to_string)
+in (FStar_Util.format3 "%s %s%s" _155_1350 (imp_to_string imp) _155_1349)))
 end
 | Let (Rec, lbs, body) -> begin
-(let _155_1341 = (to_string_l " and " (fun _60_523 -> (match (_60_523) with
+(let _155_1355 = (to_string_l " and " (fun _60_526 -> (match (_60_526) with
 | (p, b) -> begin
-(let _155_1339 = (FStar_All.pipe_right p pat_to_string)
-in (let _155_1338 = (FStar_All.pipe_right b term_to_string)
-in (FStar_Util.format2 "%s=%s" _155_1339 _155_1338)))
+(let _155_1353 = (FStar_All.pipe_right p pat_to_string)
+in (let _155_1352 = (FStar_All.pipe_right b term_to_string)
+in (FStar_Util.format2 "%s=%s" _155_1353 _155_1352)))
 end)) lbs)
-in (let _155_1340 = (FStar_All.pipe_right body term_to_string)
-in (FStar_Util.format2 "let rec %s in %s" _155_1341 _155_1340)))
+in (let _155_1354 = (FStar_All.pipe_right body term_to_string)
+in (FStar_Util.format2 "let rec %s in %s" _155_1355 _155_1354)))
 end
 | Let (q, ((pat, tm))::[], body) -> begin
-(let _155_1344 = (FStar_All.pipe_right pat pat_to_string)
-in (let _155_1343 = (FStar_All.pipe_right tm term_to_string)
-in (let _155_1342 = (FStar_All.pipe_right body term_to_string)
-in (FStar_Util.format4 "let %s %s = %s in %s" (string_of_let_qualifier q) _155_1344 _155_1343 _155_1342))))
+(let _155_1358 = (FStar_All.pipe_right pat pat_to_string)
+in (let _155_1357 = (FStar_All.pipe_right tm term_to_string)
+in (let _155_1356 = (FStar_All.pipe_right body term_to_string)
+in (FStar_Util.format4 "let %s %s = %s in %s" (string_of_let_qualifier q) _155_1358 _155_1357 _155_1356))))
 end
 | Seq (t1, t2) -> begin
-(let _155_1346 = (FStar_All.pipe_right t1 term_to_string)
-in (let _155_1345 = (FStar_All.pipe_right t2 term_to_string)
-in (FStar_Util.format2 "%s; %s" _155_1346 _155_1345)))
+(let _155_1360 = (FStar_All.pipe_right t1 term_to_string)
+in (let _155_1359 = (FStar_All.pipe_right t2 term_to_string)
+in (FStar_Util.format2 "%s; %s" _155_1360 _155_1359)))
 end
 | If (t1, t2, t3) -> begin
-(let _155_1349 = (FStar_All.pipe_right t1 term_to_string)
-in (let _155_1348 = (FStar_All.pipe_right t2 term_to_string)
-in (let _155_1347 = (FStar_All.pipe_right t3 term_to_string)
-in (FStar_Util.format3 "if %s then %s else %s" _155_1349 _155_1348 _155_1347))))
+(let _155_1363 = (FStar_All.pipe_right t1 term_to_string)
+in (let _155_1362 = (FStar_All.pipe_right t2 term_to_string)
+in (let _155_1361 = (FStar_All.pipe_right t3 term_to_string)
+in (FStar_Util.format3 "if %s then %s else %s" _155_1363 _155_1362 _155_1361))))
 end
 | Match (t, branches) -> begin
-(let _155_1356 = (FStar_All.pipe_right t term_to_string)
-in (let _155_1355 = (to_string_l " | " (fun _60_548 -> (match (_60_548) with
+(let _155_1370 = (FStar_All.pipe_right t term_to_string)
+in (let _155_1369 = (to_string_l " | " (fun _60_551 -> (match (_60_551) with
 | (p, w, e) -> begin
-(let _155_1354 = (FStar_All.pipe_right p pat_to_string)
-in (let _155_1353 = (match (w) with
+(let _155_1368 = (FStar_All.pipe_right p pat_to_string)
+in (let _155_1367 = (match (w) with
 | None -> begin
 ""
 end
 | Some (e) -> begin
-(let _155_1351 = (term_to_string e)
-in (FStar_Util.format1 "when %s" _155_1351))
+(let _155_1365 = (term_to_string e)
+in (FStar_Util.format1 "when %s" _155_1365))
 end)
-in (let _155_1352 = (FStar_All.pipe_right e term_to_string)
-in (FStar_Util.format3 "%s %s -> %s" _155_1354 _155_1353 _155_1352))))
+in (let _155_1366 = (FStar_All.pipe_right e term_to_string)
+in (FStar_Util.format3 "%s %s -> %s" _155_1368 _155_1367 _155_1366))))
 end)) branches)
-in (FStar_Util.format2 "match %s with %s" _155_1356 _155_1355)))
+in (FStar_Util.format2 "match %s with %s" _155_1370 _155_1369)))
 end
 | Ascribed (t1, t2) -> begin
-(let _155_1358 = (FStar_All.pipe_right t1 term_to_string)
-in (let _155_1357 = (FStar_All.pipe_right t2 term_to_string)
-in (FStar_Util.format2 "(%s : %s)" _155_1358 _155_1357)))
+(let _155_1372 = (FStar_All.pipe_right t1 term_to_string)
+in (let _155_1371 = (FStar_All.pipe_right t2 term_to_string)
+in (FStar_Util.format2 "(%s : %s)" _155_1372 _155_1371)))
 end
 | Record (Some (e), fields) -> begin
-(let _155_1362 = (FStar_All.pipe_right e term_to_string)
-in (let _155_1361 = (to_string_l " " (fun _60_563 -> (match (_60_563) with
+(let _155_1376 = (FStar_All.pipe_right e term_to_string)
+in (let _155_1375 = (to_string_l " " (fun _60_566 -> (match (_60_566) with
 | (l, e) -> begin
-(let _155_1360 = (FStar_All.pipe_right e term_to_string)
-in (FStar_Util.format2 "%s=%s" l.FStar_Ident.str _155_1360))
+(let _155_1374 = (FStar_All.pipe_right e term_to_string)
+in (FStar_Util.format2 "%s=%s" l.FStar_Ident.str _155_1374))
 end)) fields)
-in (FStar_Util.format2 "{%s with %s}" _155_1362 _155_1361)))
+in (FStar_Util.format2 "{%s with %s}" _155_1376 _155_1375)))
 end
 | Record (None, fields) -> begin
-(let _155_1365 = (to_string_l " " (fun _60_570 -> (match (_60_570) with
+(let _155_1379 = (to_string_l " " (fun _60_573 -> (match (_60_573) with
 | (l, e) -> begin
-(let _155_1364 = (FStar_All.pipe_right e term_to_string)
-in (FStar_Util.format2 "%s=%s" l.FStar_Ident.str _155_1364))
+(let _155_1378 = (FStar_All.pipe_right e term_to_string)
+in (FStar_Util.format2 "%s=%s" l.FStar_Ident.str _155_1378))
 end)) fields)
-in (FStar_Util.format1 "{%s}" _155_1365))
+in (FStar_Util.format1 "{%s}" _155_1379))
 end
 | Project (e, l) -> begin
-(let _155_1366 = (FStar_All.pipe_right e term_to_string)
-in (FStar_Util.format2 "%s.%s" _155_1366 l.FStar_Ident.str))
+(let _155_1380 = (FStar_All.pipe_right e term_to_string)
+in (FStar_Util.format2 "%s.%s" _155_1380 l.FStar_Ident.str))
 end
 | Product ([], t) -> begin
 (term_to_string t)
@@ -2126,51 +2142,51 @@ end
 (term_to_string (mk_term (Product ((((b)::[]), ((mk_term (Product ((((hd)::tl), (t)))) x.range x.level))))) x.range x.level))
 end
 | Product ((b)::[], t) when (x.level = Type) -> begin
-(let _155_1368 = (FStar_All.pipe_right b binder_to_string)
-in (let _155_1367 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s -> %s" _155_1368 _155_1367)))
+(let _155_1382 = (FStar_All.pipe_right b binder_to_string)
+in (let _155_1381 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s -> %s" _155_1382 _155_1381)))
 end
 | Product ((b)::[], t) when (x.level = Kind) -> begin
-(let _155_1370 = (FStar_All.pipe_right b binder_to_string)
-in (let _155_1369 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s => %s" _155_1370 _155_1369)))
+(let _155_1384 = (FStar_All.pipe_right b binder_to_string)
+in (let _155_1383 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s => %s" _155_1384 _155_1383)))
 end
 | Sum (binders, t) -> begin
-(let _155_1373 = (let _155_1371 = (FStar_All.pipe_right binders (FStar_List.map binder_to_string))
-in (FStar_All.pipe_right _155_1371 (FStar_String.concat " * ")))
-in (let _155_1372 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s * %s" _155_1373 _155_1372)))
+(let _155_1387 = (let _155_1385 = (FStar_All.pipe_right binders (FStar_List.map binder_to_string))
+in (FStar_All.pipe_right _155_1385 (FStar_String.concat " * ")))
+in (let _155_1386 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s * %s" _155_1387 _155_1386)))
 end
 | QForall (bs, pats, t) -> begin
-(let _155_1376 = (to_string_l " " binder_to_string bs)
-in (let _155_1375 = (to_string_l " \\/ " (to_string_l "; " term_to_string) pats)
-in (let _155_1374 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format3 "forall %s.{:pattern %s} %s" _155_1376 _155_1375 _155_1374))))
+(let _155_1390 = (to_string_l " " binder_to_string bs)
+in (let _155_1389 = (to_string_l " \\/ " (to_string_l "; " term_to_string) pats)
+in (let _155_1388 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format3 "forall %s.{:pattern %s} %s" _155_1390 _155_1389 _155_1388))))
 end
 | QExists (bs, pats, t) -> begin
-(let _155_1379 = (to_string_l " " binder_to_string bs)
-in (let _155_1378 = (to_string_l " \\/ " (to_string_l "; " term_to_string) pats)
-in (let _155_1377 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format3 "exists %s.{:pattern %s} %s" _155_1379 _155_1378 _155_1377))))
+(let _155_1393 = (to_string_l " " binder_to_string bs)
+in (let _155_1392 = (to_string_l " \\/ " (to_string_l "; " term_to_string) pats)
+in (let _155_1391 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format3 "exists %s.{:pattern %s} %s" _155_1393 _155_1392 _155_1391))))
 end
 | Refine (b, t) -> begin
-(let _155_1381 = (FStar_All.pipe_right b binder_to_string)
-in (let _155_1380 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s:{%s}" _155_1381 _155_1380)))
+(let _155_1395 = (FStar_All.pipe_right b binder_to_string)
+in (let _155_1394 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s:{%s}" _155_1395 _155_1394)))
 end
 | NamedTyp (x, t) -> begin
-(let _155_1382 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s:%s" x.FStar_Ident.idText _155_1382))
+(let _155_1396 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s:%s" x.FStar_Ident.idText _155_1396))
 end
 | Paren (t) -> begin
-(let _155_1383 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format1 "(%s)" _155_1383))
+(let _155_1397 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format1 "(%s)" _155_1397))
 end
 | Product (bs, t) -> begin
-(let _155_1386 = (let _155_1384 = (FStar_All.pipe_right bs (FStar_List.map binder_to_string))
-in (FStar_All.pipe_right _155_1384 (FStar_String.concat ",")))
-in (let _155_1385 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "Unidentified product: [%s] %s" _155_1386 _155_1385)))
+(let _155_1400 = (let _155_1398 = (FStar_All.pipe_right bs (FStar_List.map binder_to_string))
+in (FStar_All.pipe_right _155_1398 (FStar_String.concat ",")))
+in (let _155_1399 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "Unidentified product: [%s] %s" _155_1400 _155_1399)))
 end
 | t -> begin
 "_"
@@ -2185,14 +2201,14 @@ end
 (FStar_Util.format1 "%s:_" i.FStar_Ident.idText)
 end
 | (TAnnotated (i, t)) | (Annotated (i, t)) -> begin
-(let _155_1388 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "%s:%s" i.FStar_Ident.idText _155_1388))
+(let _155_1402 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "%s:%s" i.FStar_Ident.idText _155_1402))
 end
 | NoName (t) -> begin
 (FStar_All.pipe_right t term_to_string)
 end)
-in (let _155_1389 = (aqual_to_string x.aqual)
-in (FStar_Util.format2 "%s%s" _155_1389 s))))
+in (let _155_1403 = (aqual_to_string x.aqual)
+in (FStar_Util.format2 "%s%s" _155_1403 s))))
 and aqual_to_string : aqual  ->  Prims.string = (fun _60_3 -> (match (_60_3) with
 | Some (Equality) -> begin
 "$"
@@ -2200,7 +2216,7 @@ end
 | Some (Implicit) -> begin
 "#"
 end
-| _60_646 -> begin
+| _60_649 -> begin
 ""
 end))
 and pat_to_string : pattern  ->  Prims.string = (fun x -> (match (x.pat) with
@@ -2211,36 +2227,36 @@ end
 (FStar_Absyn_Print.const_to_string c)
 end
 | PatApp (p, ps) -> begin
-(let _155_1393 = (FStar_All.pipe_right p pat_to_string)
-in (let _155_1392 = (to_string_l " " pat_to_string ps)
-in (FStar_Util.format2 "(%s %s)" _155_1393 _155_1392)))
+(let _155_1407 = (FStar_All.pipe_right p pat_to_string)
+in (let _155_1406 = (to_string_l " " pat_to_string ps)
+in (FStar_Util.format2 "(%s %s)" _155_1407 _155_1406)))
 end
 | (PatTvar (i, aq)) | (PatVar (i, aq)) -> begin
-(let _155_1394 = (aqual_to_string aq)
-in (FStar_Util.format2 "%s%s" _155_1394 i.FStar_Ident.idText))
+(let _155_1408 = (aqual_to_string aq)
+in (FStar_Util.format2 "%s%s" _155_1408 i.FStar_Ident.idText))
 end
 | PatName (l) -> begin
 l.FStar_Ident.str
 end
 | PatList (l) -> begin
-(let _155_1395 = (to_string_l "; " pat_to_string l)
-in (FStar_Util.format1 "[%s]" _155_1395))
+(let _155_1409 = (to_string_l "; " pat_to_string l)
+in (FStar_Util.format1 "[%s]" _155_1409))
 end
 | PatTuple (l, false) -> begin
-(let _155_1396 = (to_string_l ", " pat_to_string l)
-in (FStar_Util.format1 "(%s)" _155_1396))
+(let _155_1410 = (to_string_l ", " pat_to_string l)
+in (FStar_Util.format1 "(%s)" _155_1410))
 end
 | PatTuple (l, true) -> begin
-(let _155_1397 = (to_string_l ", " pat_to_string l)
-in (FStar_Util.format1 "(|%s|)" _155_1397))
+(let _155_1411 = (to_string_l ", " pat_to_string l)
+in (FStar_Util.format1 "(|%s|)" _155_1411))
 end
 | PatRecord (l) -> begin
-(let _155_1400 = (to_string_l "; " (fun _60_677 -> (match (_60_677) with
+(let _155_1414 = (to_string_l "; " (fun _60_680 -> (match (_60_680) with
 | (f, e) -> begin
-(let _155_1399 = (FStar_All.pipe_right e pat_to_string)
-in (FStar_Util.format2 "%s=%s" f.FStar_Ident.str _155_1399))
+(let _155_1413 = (FStar_All.pipe_right e pat_to_string)
+in (FStar_Util.format2 "%s=%s" f.FStar_Ident.str _155_1413))
 end)) l)
-in (FStar_Util.format1 "{%s}" _155_1400))
+in (FStar_Util.format1 "{%s}" _155_1414))
 end
 | PatOr (l) -> begin
 (to_string_l "|\n " pat_to_string l)
@@ -2249,9 +2265,9 @@ end
 (FStar_Util.format1 "(%s)" op)
 end
 | PatAscribed (p, t) -> begin
-(let _155_1402 = (FStar_All.pipe_right p pat_to_string)
-in (let _155_1401 = (FStar_All.pipe_right t term_to_string)
-in (FStar_Util.format2 "(%s:%s)" _155_1402 _155_1401)))
+(let _155_1416 = (FStar_All.pipe_right p pat_to_string)
+in (let _155_1415 = (FStar_All.pipe_right t term_to_string)
+in (FStar_Util.format2 "(%s:%s)" _155_1416 _155_1415)))
 end))
 
 
@@ -2259,23 +2275,23 @@ let rec head_id_of_pat : pattern  ->  FStar_Ident.lid Prims.list = (fun p -> (ma
 | PatName (l) -> begin
 (l)::[]
 end
-| PatVar (i, _60_691) -> begin
-(let _155_1405 = (FStar_Ident.lid_of_ids ((i)::[]))
-in (_155_1405)::[])
+| PatVar (i, _60_694) -> begin
+(let _155_1419 = (FStar_Ident.lid_of_ids ((i)::[]))
+in (_155_1419)::[])
 end
-| PatApp (p, _60_696) -> begin
+| PatApp (p, _60_699) -> begin
 (head_id_of_pat p)
 end
-| PatAscribed (p, _60_701) -> begin
+| PatAscribed (p, _60_704) -> begin
 (head_id_of_pat p)
 end
-| _60_705 -> begin
+| _60_708 -> begin
 []
 end))
 
 
-let lids_of_let = (fun defs -> (FStar_All.pipe_right defs (FStar_List.collect (fun _60_710 -> (match (_60_710) with
-| (p, _60_709) -> begin
+let lids_of_let = (fun defs -> (FStar_All.pipe_right defs (FStar_List.collect (fun _60_713 -> (match (_60_713) with
+| (p, _60_712) -> begin
 (head_id_of_pat p)
 end)))))
 
@@ -2293,36 +2309,39 @@ end
 | Open (l) -> begin
 (Prims.strcat "open " l.FStar_Ident.str)
 end
+| Include (l) -> begin
+(Prims.strcat "include " l.FStar_Ident.str)
+end
 | ModuleAbbrev (i, l) -> begin
 (FStar_Util.format2 "module %s = %s" i.FStar_Ident.idText l.FStar_Ident.str)
 end
-| KindAbbrev (i, _60_754, _60_756) -> begin
+| KindAbbrev (i, _60_759, _60_761) -> begin
 (Prims.strcat "kind " i.FStar_Ident.idText)
 end
-| TopLevelLet (_60_760, _60_762, pats) -> begin
-(let _155_1415 = (let _155_1414 = (let _155_1413 = (lids_of_let pats)
-in (FStar_All.pipe_right _155_1413 (FStar_List.map (fun l -> l.FStar_Ident.str))))
-in (FStar_All.pipe_right _155_1414 (FStar_String.concat ", ")))
-in (Prims.strcat "let " _155_1415))
+| TopLevelLet (_60_765, _60_767, pats) -> begin
+(let _155_1429 = (let _155_1428 = (let _155_1427 = (lids_of_let pats)
+in (FStar_All.pipe_right _155_1427 (FStar_List.map (fun l -> l.FStar_Ident.str))))
+in (FStar_All.pipe_right _155_1428 (FStar_String.concat ", ")))
+in (Prims.strcat "let " _155_1429))
 end
-| Main (_60_768) -> begin
+| Main (_60_773) -> begin
 "main ..."
 end
-| Assume (_60_771, i, _60_774) -> begin
+| Assume (_60_776, i, _60_779) -> begin
 (Prims.strcat "assume " i.FStar_Ident.idText)
 end
-| Tycon (_60_778, tys) -> begin
-(let _155_1418 = (let _155_1417 = (FStar_All.pipe_right tys (FStar_List.map (fun _60_785 -> (match (_60_785) with
-| (x, _60_784) -> begin
+| Tycon (_60_783, tys) -> begin
+(let _155_1432 = (let _155_1431 = (FStar_All.pipe_right tys (FStar_List.map (fun _60_790 -> (match (_60_790) with
+| (x, _60_789) -> begin
 (id_of_tycon x)
 end))))
-in (FStar_All.pipe_right _155_1417 (FStar_String.concat ", ")))
-in (Prims.strcat "type " _155_1418))
+in (FStar_All.pipe_right _155_1431 (FStar_String.concat ", ")))
+in (Prims.strcat "type " _155_1432))
 end
-| Val (_60_787, i, _60_790) -> begin
+| Val (_60_792, i, _60_795) -> begin
 (Prims.strcat "val " i.FStar_Ident.idText)
 end
-| Exception (i, _60_795) -> begin
+| Exception (i, _60_800) -> begin
 (Prims.strcat "exception " i.FStar_Ident.idText)
 end
 | (NewEffect (_, DefineEffect (i, _, _, _, _))) | (NewEffect (_, RedefineEffect (i, _, _))) -> begin
@@ -2331,21 +2350,21 @@ end
 | (NewEffectForFree (_, DefineEffect (i, _, _, _, _))) | (NewEffectForFree (_, RedefineEffect (i, _, _))) -> begin
 (Prims.strcat "new_effect_for_free " i.FStar_Ident.idText)
 end
-| SubEffect (_60_849) -> begin
+| SubEffect (_60_854) -> begin
 "sub_effect"
 end
-| Pragma (_60_852) -> begin
+| Pragma (_60_857) -> begin
 "pragma"
 end
-| Fsdoc (_60_855) -> begin
+| Fsdoc (_60_860) -> begin
 "fsdoc"
 end))
 
 
 let modul_to_string : modul  ->  Prims.string = (fun m -> (match (m) with
 | (Module (_, decls)) | (Interface (_, decls, _)) -> begin
-(let _155_1421 = (FStar_All.pipe_right decls (FStar_List.map decl_to_string))
-in (FStar_All.pipe_right _155_1421 (FStar_String.concat "\n")))
+(let _155_1435 = (FStar_All.pipe_right decls (FStar_List.map decl_to_string))
+in (FStar_All.pipe_right _155_1435 (FStar_String.concat "\n")))
 end))
 
 
@@ -2355,8 +2374,8 @@ let tm = (FStar_All.pipe_right tm term_to_string)
 in (
 
 let tm = if ((FStar_String.length tm) >= (Prims.parse_int "80")) then begin
-(let _155_1425 = (FStar_Util.substring tm (Prims.parse_int "0") (Prims.parse_int "77"))
-in (Prims.strcat _155_1425 "..."))
+(let _155_1439 = (FStar_Util.substring tm (Prims.parse_int "0") (Prims.parse_int "77"))
+in (Prims.strcat _155_1439 "..."))
 end else begin
 tm
 end
diff --git a/src/ocaml-output/FStar_Parser_Dep.ml b/src/ocaml-output/FStar_Parser_Dep.ml
index 6d8a64143f2..e399fb3714f 100755
--- a/src/ocaml-output/FStar_Parser_Dep.ml
+++ b/src/ocaml-output/FStar_Parser_Dep.ml
@@ -436,50 +436,50 @@ in (collect_decls decls)))
 end))
 and collect_decls = (fun decls -> (FStar_List.iter (fun x -> (collect_decl x.FStar_Parser_AST.d)) decls))
 and collect_decl = (fun _70_5 -> (match (_70_5) with
-| FStar_Parser_AST.Open (lid) -> begin
+| (FStar_Parser_AST.Include (lid)) | (FStar_Parser_AST.Open (lid)) -> begin
 (record_open false lid)
 end
 | FStar_Parser_AST.ModuleAbbrev (ident, lid) -> begin
 (
 
-let _70_207 = (let _165_150 = (lowercase_join_longident lid true)
+let _70_208 = (let _165_150 = (lowercase_join_longident lid true)
 in (add_dep _165_150))
 in (record_module_alias ident lid))
 end
-| FStar_Parser_AST.TopLevelLet (_70_210, _70_212, patterms) -> begin
-(FStar_List.iter (fun _70_218 -> (match (_70_218) with
+| FStar_Parser_AST.TopLevelLet (_70_211, _70_213, patterms) -> begin
+(FStar_List.iter (fun _70_219 -> (match (_70_219) with
 | (pat, t) -> begin
 (
 
-let _70_219 = (collect_pattern pat)
+let _70_220 = (collect_pattern pat)
 in (collect_term t))
 end)) patterms)
 end
-| FStar_Parser_AST.KindAbbrev (_70_222, binders, t) -> begin
+| FStar_Parser_AST.KindAbbrev (_70_223, binders, t) -> begin
 (
 
-let _70_227 = (collect_term t)
+let _70_228 = (collect_term t)
 in (collect_binders binders))
 end
 | (FStar_Parser_AST.Main (t)) | (FStar_Parser_AST.Assume (_, _, t)) | (FStar_Parser_AST.SubEffect ({FStar_Parser_AST.msource = _; FStar_Parser_AST.mdest = _; FStar_Parser_AST.lift_op = FStar_Parser_AST.NonReifiableLift (t)})) | (FStar_Parser_AST.SubEffect ({FStar_Parser_AST.msource = _; FStar_Parser_AST.mdest = _; FStar_Parser_AST.lift_op = FStar_Parser_AST.LiftForFree (t)})) | (FStar_Parser_AST.Val (_, _, t)) -> begin
 (collect_term t)
 end
-| FStar_Parser_AST.SubEffect ({FStar_Parser_AST.msource = _70_264; FStar_Parser_AST.mdest = _70_262; FStar_Parser_AST.lift_op = FStar_Parser_AST.ReifiableLift (t0, t1)}) -> begin
+| FStar_Parser_AST.SubEffect ({FStar_Parser_AST.msource = _70_265; FStar_Parser_AST.mdest = _70_263; FStar_Parser_AST.lift_op = FStar_Parser_AST.ReifiableLift (t0, t1)}) -> begin
 (
 
-let _70_267 = (collect_term t0)
+let _70_268 = (collect_term t0)
 in (collect_term t1))
 end
-| FStar_Parser_AST.Tycon (_70_270, ts) -> begin
+| FStar_Parser_AST.Tycon (_70_271, ts) -> begin
 (
 
-let ts = (FStar_List.map (fun _70_276 -> (match (_70_276) with
+let ts = (FStar_List.map (fun _70_277 -> (match (_70_277) with
 | (x, doc) -> begin
 x
 end)) ts)
 in (FStar_List.iter collect_tycon ts))
 end
-| FStar_Parser_AST.Exception (_70_279, t) -> begin
+| FStar_Parser_AST.Exception (_70_280, t) -> begin
 (FStar_Util.iter_opt t collect_term)
 end
 | (FStar_Parser_AST.NewEffectForFree (_, ed)) | (FStar_Parser_AST.NewEffect (_, ed)) -> begin
@@ -491,7 +491,7 @@ end
 | FStar_Parser_AST.TopLevelModule (lid) -> begin
 (
 
-let _70_300 = (FStar_Util.incr num_of_toplevelmods)
+let _70_301 = (FStar_Util.incr num_of_toplevelmods)
 in if ((FStar_ST.read num_of_toplevelmods) > (Prims.parse_int "1")) then begin
 (let _165_155 = (let _165_154 = (let _165_153 = (string_of_lid lid true)
 in (FStar_Util.format1 "Automatic dependency analysis demands one module per file (module %s not supported)" _165_153))
@@ -502,62 +502,62 @@ end else begin
 end)
 end))
 and collect_tycon = (fun _70_6 -> (match (_70_6) with
-| FStar_Parser_AST.TyconAbstract (_70_304, binders, k) -> begin
+| FStar_Parser_AST.TyconAbstract (_70_305, binders, k) -> begin
 (
 
-let _70_309 = (collect_binders binders)
+let _70_310 = (collect_binders binders)
 in (FStar_Util.iter_opt k collect_term))
 end
-| FStar_Parser_AST.TyconAbbrev (_70_312, binders, k, t) -> begin
+| FStar_Parser_AST.TyconAbbrev (_70_313, binders, k, t) -> begin
 (
 
-let _70_318 = (collect_binders binders)
+let _70_319 = (collect_binders binders)
 in (
 
-let _70_320 = (FStar_Util.iter_opt k collect_term)
+let _70_321 = (FStar_Util.iter_opt k collect_term)
 in (collect_term t)))
 end
-| FStar_Parser_AST.TyconRecord (_70_323, binders, k, identterms) -> begin
+| FStar_Parser_AST.TyconRecord (_70_324, binders, k, identterms) -> begin
 (
 
-let _70_329 = (collect_binders binders)
+let _70_330 = (collect_binders binders)
 in (
 
-let _70_331 = (FStar_Util.iter_opt k collect_term)
-in (FStar_List.iter (fun _70_338 -> (match (_70_338) with
-| (_70_334, t, _70_337) -> begin
+let _70_332 = (FStar_Util.iter_opt k collect_term)
+in (FStar_List.iter (fun _70_339 -> (match (_70_339) with
+| (_70_335, t, _70_338) -> begin
 (collect_term t)
 end)) identterms)))
 end
-| FStar_Parser_AST.TyconVariant (_70_340, binders, k, identterms) -> begin
+| FStar_Parser_AST.TyconVariant (_70_341, binders, k, identterms) -> begin
 (
 
-let _70_346 = (collect_binders binders)
+let _70_347 = (collect_binders binders)
 in (
 
-let _70_348 = (FStar_Util.iter_opt k collect_term)
-in (FStar_List.iter (fun _70_357 -> (match (_70_357) with
-| (_70_351, t, _70_354, _70_356) -> begin
+let _70_349 = (FStar_Util.iter_opt k collect_term)
+in (FStar_List.iter (fun _70_358 -> (match (_70_358) with
+| (_70_352, t, _70_355, _70_357) -> begin
 (FStar_Util.iter_opt t collect_term)
 end)) identterms)))
 end))
 and collect_effect_decl = (fun _70_7 -> (match (_70_7) with
-| FStar_Parser_AST.DefineEffect (_70_360, binders, t, decls, actions) -> begin
+| FStar_Parser_AST.DefineEffect (_70_361, binders, t, decls, actions) -> begin
 (
 
-let _70_367 = (collect_binders binders)
+let _70_368 = (collect_binders binders)
 in (
 
-let _70_369 = (collect_term t)
+let _70_370 = (collect_term t)
 in (
 
-let _70_371 = (collect_decls decls)
+let _70_372 = (collect_decls decls)
 in (collect_decls actions))))
 end
-| FStar_Parser_AST.RedefineEffect (_70_374, binders, t) -> begin
+| FStar_Parser_AST.RedefineEffect (_70_375, binders, t) -> begin
 (
 
-let _70_379 = (collect_binders binders)
+let _70_380 = (collect_binders binders)
 in (collect_term t))
 end))
 and collect_binders = (fun binders -> (FStar_List.iter collect_binder binders))
@@ -565,12 +565,12 @@ and collect_binder = (fun _70_8 -> (match (_70_8) with
 | ({FStar_Parser_AST.b = FStar_Parser_AST.Annotated (_, t); FStar_Parser_AST.brange = _; FStar_Parser_AST.blevel = _; FStar_Parser_AST.aqual = _}) | ({FStar_Parser_AST.b = FStar_Parser_AST.TAnnotated (_, t); FStar_Parser_AST.brange = _; FStar_Parser_AST.blevel = _; FStar_Parser_AST.aqual = _}) | ({FStar_Parser_AST.b = FStar_Parser_AST.NoName (t); FStar_Parser_AST.brange = _; FStar_Parser_AST.blevel = _; FStar_Parser_AST.aqual = _}) -> begin
 (collect_term t)
 end
-| _70_415 -> begin
+| _70_416 -> begin
 ()
 end))
 and collect_term = (fun t -> (collect_term' t.FStar_Parser_AST.tm))
 and collect_constant = (fun _70_9 -> (match (_70_9) with
-| FStar_Const.Const_int (_70_419, Some (signedness, width)) -> begin
+| FStar_Const.Const_int (_70_420, Some (signedness, width)) -> begin
 (
 
 let u = (match (signedness) with
@@ -598,7 +598,7 @@ end)
 in (let _165_164 = (FStar_Util.format2 "fstar.%sint%s" u w)
 in (add_dep _165_164))))
 end
-| _70_435 -> begin
+| _70_436 -> begin
 ()
 end))
 and collect_term' = (fun _70_10 -> (match (_70_10) with
@@ -611,7 +611,7 @@ end
 | FStar_Parser_AST.Op (s, ts) -> begin
 (
 
-let _70_444 = if (s = "@") then begin
+let _70_445 = if (s = "@") then begin
 (let _165_167 = (let _165_166 = (FStar_Ident.lid_of_path (FStar_Ident.path_of_text "FStar.List.Tot.append") FStar_Range.dummyRange)
 in FStar_Parser_AST.Name (_165_166))
 in (collect_term' _165_167))
@@ -620,7 +620,7 @@ end else begin
 end
 in (FStar_List.iter collect_term ts))
 end
-| FStar_Parser_AST.Tvar (_70_447) -> begin
+| FStar_Parser_AST.Tvar (_70_448) -> begin
 ()
 end
 | (FStar_Parser_AST.Var (lid)) | (FStar_Parser_AST.Projector (lid, _)) | (FStar_Parser_AST.Discrim (lid)) | (FStar_Parser_AST.Name (lid)) -> begin
@@ -629,36 +629,36 @@ end
 | FStar_Parser_AST.Construct (lid, termimps) -> begin
 (
 
-let _70_461 = if (((FStar_List.length termimps) = (Prims.parse_int "1")) && (FStar_Options.universes ())) then begin
+let _70_462 = if (((FStar_List.length termimps) = (Prims.parse_int "1")) && (FStar_Options.universes ())) then begin
 (record_lid true lid)
 end else begin
 ()
 end
-in (FStar_List.iter (fun _70_466 -> (match (_70_466) with
-| (t, _70_465) -> begin
+in (FStar_List.iter (fun _70_467 -> (match (_70_467) with
+| (t, _70_466) -> begin
 (collect_term t)
 end)) termimps))
 end
 | FStar_Parser_AST.Abs (pats, t) -> begin
 (
 
-let _70_471 = (collect_patterns pats)
+let _70_472 = (collect_patterns pats)
 in (collect_term t))
 end
-| FStar_Parser_AST.App (t1, t2, _70_476) -> begin
+| FStar_Parser_AST.App (t1, t2, _70_477) -> begin
 (
 
-let _70_479 = (collect_term t1)
+let _70_480 = (collect_term t1)
 in (collect_term t2))
 end
-| FStar_Parser_AST.Let (_70_482, patterms, t) -> begin
+| FStar_Parser_AST.Let (_70_483, patterms, t) -> begin
 (
 
-let _70_492 = (FStar_List.iter (fun _70_489 -> (match (_70_489) with
+let _70_493 = (FStar_List.iter (fun _70_490 -> (match (_70_490) with
 | (pat, t) -> begin
 (
 
-let _70_490 = (collect_pattern pat)
+let _70_491 = (collect_pattern pat)
 in (collect_term t))
 end)) patterms)
 in (collect_term t))
@@ -666,70 +666,70 @@ end
 | FStar_Parser_AST.LetOpen (lid, t) -> begin
 (
 
-let _70_498 = (record_open true lid)
+let _70_499 = (record_open true lid)
 in (collect_term t))
 end
 | FStar_Parser_AST.Seq (t1, t2) -> begin
 (
 
-let _70_504 = (collect_term t1)
+let _70_505 = (collect_term t1)
 in (collect_term t2))
 end
 | FStar_Parser_AST.If (t1, t2, t3) -> begin
 (
 
-let _70_511 = (collect_term t1)
+let _70_512 = (collect_term t1)
 in (
 
-let _70_513 = (collect_term t2)
+let _70_514 = (collect_term t2)
 in (collect_term t3)))
 end
 | (FStar_Parser_AST.Match (t, bs)) | (FStar_Parser_AST.TryWith (t, bs)) -> begin
 (
 
-let _70_521 = (collect_term t)
+let _70_522 = (collect_term t)
 in (collect_branches bs))
 end
 | FStar_Parser_AST.Ascribed (t1, t2) -> begin
 (
 
-let _70_527 = (collect_term t1)
+let _70_528 = (collect_term t1)
 in (collect_term t2))
 end
 | FStar_Parser_AST.Record (t, idterms) -> begin
 (
 
-let _70_533 = (FStar_Util.iter_opt t collect_term)
-in (FStar_List.iter (fun _70_538 -> (match (_70_538) with
-| (_70_536, t) -> begin
+let _70_534 = (FStar_Util.iter_opt t collect_term)
+in (FStar_List.iter (fun _70_539 -> (match (_70_539) with
+| (_70_537, t) -> begin
 (collect_term t)
 end)) idterms))
 end
-| FStar_Parser_AST.Project (t, _70_541) -> begin
+| FStar_Parser_AST.Project (t, _70_542) -> begin
 (collect_term t)
 end
 | (FStar_Parser_AST.Product (binders, t)) | (FStar_Parser_AST.Sum (binders, t)) -> begin
 (
 
-let _70_550 = (collect_binders binders)
+let _70_551 = (collect_binders binders)
 in (collect_term t))
 end
 | (FStar_Parser_AST.QForall (binders, ts, t)) | (FStar_Parser_AST.QExists (binders, ts, t)) -> begin
 (
 
-let _70_559 = (collect_binders binders)
+let _70_560 = (collect_binders binders)
 in (
 
-let _70_561 = (FStar_List.iter (FStar_List.iter collect_term) ts)
+let _70_562 = (FStar_List.iter (FStar_List.iter collect_term) ts)
 in (collect_term t)))
 end
 | FStar_Parser_AST.Refine (binder, t) -> begin
 (
 
-let _70_567 = (collect_binder binder)
+let _70_568 = (collect_binder binder)
 in (collect_term t))
 end
-| FStar_Parser_AST.NamedTyp (_70_570, t) -> begin
+| FStar_Parser_AST.NamedTyp (_70_571, t) -> begin
 (collect_term t)
 end
 | FStar_Parser_AST.Paren (t) -> begin
@@ -747,7 +747,7 @@ end
 | FStar_Parser_AST.PatApp (p, ps) -> begin
 (
 
-let _70_609 = (collect_pattern p)
+let _70_610 = (collect_pattern p)
 in (collect_patterns ps))
 end
 | (FStar_Parser_AST.PatVar (_)) | (FStar_Parser_AST.PatName (_)) | (FStar_Parser_AST.PatTvar (_)) -> begin
@@ -757,26 +757,26 @@ end
 (collect_patterns ps)
 end
 | FStar_Parser_AST.PatRecord (lidpats) -> begin
-(FStar_List.iter (fun _70_632 -> (match (_70_632) with
-| (_70_630, p) -> begin
+(FStar_List.iter (fun _70_633 -> (match (_70_633) with
+| (_70_631, p) -> begin
 (collect_pattern p)
 end)) lidpats)
 end
 | FStar_Parser_AST.PatAscribed (p, t) -> begin
 (
 
-let _70_637 = (collect_pattern p)
+let _70_638 = (collect_pattern p)
 in (collect_term t))
 end))
 and collect_branches = (fun bs -> (FStar_List.iter collect_branch bs))
-and collect_branch = (fun _70_643 -> (match (_70_643) with
+and collect_branch = (fun _70_644 -> (match (_70_644) with
 | (pat, t1, t2) -> begin
 (
 
-let _70_644 = (collect_pattern pat)
+let _70_645 = (collect_pattern pat)
 in (
 
-let _70_646 = (FStar_Util.iter_opt t1 collect_term)
+let _70_647 = (FStar_Util.iter_opt t1 collect_term)
 in (collect_term t2)))
 end))
 in (
@@ -784,7 +784,7 @@ in (
 let ast = (FStar_Parser_Driver.parse_file filename)
 in (
 
-let _70_649 = (collect_file ast)
+let _70_650 = (collect_file ast)
 in (FStar_ST.read deps))))))))))))))
 
 
@@ -823,13 +823,13 @@ end))
 
 let print_graph = (fun graph -> (
 
-let _70_652 = (FStar_Util.print_endline "A DOT-format graph has been dumped in the current directory as dep.graph")
+let _70_653 = (FStar_Util.print_endline "A DOT-format graph has been dumped in the current directory as dep.graph")
 in (
 
-let _70_654 = (FStar_Util.print_endline "With GraphViz installed, try: fdp -Tpng -odep.png dep.graph")
+let _70_655 = (FStar_Util.print_endline "With GraphViz installed, try: fdp -Tpng -odep.png dep.graph")
 in (
 
-let _70_656 = (FStar_Util.print_endline "Hint: cat dep.graph | grep -v _ | grep -v prims")
+let _70_657 = (FStar_Util.print_endline "Hint: cat dep.graph | grep -v _ | grep -v prims")
 in (let _165_192 = (let _165_191 = (let _165_190 = (let _165_189 = (let _165_188 = (let _165_187 = (FStar_Util.smap_keys graph)
 in (FStar_List.unique _165_187))
 in (FStar_List.collect (fun k -> (
@@ -866,9 +866,9 @@ in (
 let rec discover_one = (fun is_user_provided_filename key -> if ((FStar_Util.smap_try_find graph key) = None) then begin
 (
 
-let _70_675 = (let _165_207 = (FStar_Util.smap_try_find m key)
+let _70_676 = (let _165_207 = (FStar_Util.smap_try_find m key)
 in (FStar_Util.must _165_207))
-in (match (_70_675) with
+in (match (_70_676) with
 | (intf, impl) -> begin
 (
 
@@ -893,7 +893,7 @@ in (
 let deps = (FStar_List.unique (FStar_List.append impl_deps intf_deps))
 in (
 
-let _70_685 = (FStar_Util.smap_add graph key ((deps), (White)))
+let _70_686 = (FStar_Util.smap_add graph key ((deps), (White)))
 in (FStar_List.iter (discover_one false) deps)))))
 end))
 end else begin
@@ -901,7 +901,7 @@ end else begin
 end)
 in (
 
-let _70_687 = (let _165_208 = (FStar_List.map lowercase_module_name filenames)
+let _70_688 = (let _165_208 = (FStar_List.map lowercase_module_name filenames)
 in (FStar_List.iter (discover_one true) _165_208))
 in (
 
@@ -913,24 +913,24 @@ in (
 
 let rec discover = (fun cycle key -> (
 
-let _70_696 = (let _165_213 = (FStar_Util.smap_try_find graph key)
+let _70_697 = (let _165_213 = (FStar_Util.smap_try_find graph key)
 in (FStar_Util.must _165_213))
-in (match (_70_696) with
+in (match (_70_697) with
 | (direct_deps, color) -> begin
 (match (color) with
 | Gray -> begin
 (
 
-let _70_698 = (FStar_Util.print1 "Warning: recursive dependency on module %s\n" key)
+let _70_699 = (FStar_Util.print1 "Warning: recursive dependency on module %s\n" key)
 in (
 
-let _70_700 = (FStar_Util.print1 "The cycle is: %s \n" (FStar_String.concat " -> " cycle))
+let _70_701 = (FStar_Util.print1 "The cycle is: %s \n" (FStar_String.concat " -> " cycle))
 in (
 
-let _70_702 = (print_graph immediate_graph)
+let _70_703 = (print_graph immediate_graph)
 in (
 
-let _70_704 = (FStar_Util.print_string "\n")
+let _70_705 = (FStar_Util.print_string "\n")
 in (FStar_All.exit (Prims.parse_int "1"))))))
 end
 | Black -> begin
@@ -939,7 +939,7 @@ end
 | White -> begin
 (
 
-let _70_708 = (FStar_Util.smap_add graph key ((direct_deps), (Gray)))
+let _70_709 = (FStar_Util.smap_add graph key ((direct_deps), (Gray)))
 in (
 
 let all_deps = (let _165_217 = (let _165_216 = (FStar_List.map (fun dep -> (let _165_215 = (discover ((key)::cycle) dep)
@@ -948,10 +948,10 @@ in (FStar_List.flatten _165_216))
 in (FStar_List.unique _165_217))
 in (
 
-let _70_712 = (FStar_Util.smap_add graph key ((all_deps), (Black)))
+let _70_713 = (FStar_Util.smap_add graph key ((all_deps), (Black)))
 in (
 
-let _70_714 = (let _165_219 = (let _165_218 = (FStar_ST.read topologically_sorted)
+let _70_715 = (let _165_219 = (let _165_218 = (FStar_ST.read topologically_sorted)
 in (key)::_165_218)
 in (FStar_ST.op_Colon_Equals topologically_sorted _165_219))
 in all_deps))))
@@ -1004,7 +1004,7 @@ let topologically_sorted = (let _165_230 = (FStar_ST.read topologically_sorted)
 in (FStar_List.collect must_find_r _165_230))
 in (
 
-let _70_734 = (FStar_List.iter (fun _70_733 -> (match (_70_733) with
+let _70_735 = (FStar_List.iter (fun _70_734 -> (match (_70_734) with
 | (m, r) -> begin
 if ((not ((FStar_ST.read r))) && (not ((FStar_Options.interactive ())))) then begin
 (let _165_233 = (let _165_232 = (FStar_Util.format2 "You passed --verify_module %s but I found no file that contains [module %s] in the dependency graph\n" m m)
@@ -1017,7 +1017,7 @@ end)) verify_flags)
 in ((by_target), (topologically_sorted), (immediate_graph))))))))))))))))))
 
 
-let print_make : (Prims.string * Prims.string Prims.list) Prims.list  ->  Prims.unit = (fun deps -> (FStar_List.iter (fun _70_739 -> (match (_70_739) with
+let print_make : (Prims.string * Prims.string Prims.list) Prims.list  ->  Prims.unit = (fun deps -> (FStar_List.iter (fun _70_740 -> (match (_70_740) with
 | (f, deps) -> begin
 (
 
@@ -1026,8 +1026,8 @@ in (FStar_Util.print2 "%s: %s\n" f (FStar_String.concat " " deps)))
 end)) deps))
 
 
-let print = (fun _70_746 -> (match (_70_746) with
-| (make_deps, _70_744, graph) -> begin
+let print = (fun _70_747 -> (match (_70_747) with
+| (make_deps, _70_745, graph) -> begin
 (match ((FStar_Options.dep ())) with
 | Some ("make") -> begin
 (print_make make_deps)
@@ -1035,7 +1035,7 @@ end
 | Some ("graph") -> begin
 (print_graph graph)
 end
-| Some (_70_752) -> begin
+| Some (_70_753) -> begin
 (Prims.raise (FStar_Absyn_Syntax.Err ("unknown tool for --dep\n")))
 end
 | None -> begin
diff --git a/src/ocaml-output/FStar_Parser_Desugar.ml b/src/ocaml-output/FStar_Parser_Desugar.ml
index 42925d2e8ea..40b60dba4c5 100755
--- a/src/ocaml-output/FStar_Parser_Desugar.ml
+++ b/src/ocaml-output/FStar_Parser_Desugar.ml
@@ -3638,6 +3638,9 @@ end
 let env = (FStar_Parser_DesugarEnv.push_namespace env lid)
 in ((env), ([])))
 end
+| FStar_Parser_AST.Include (_62_2869) -> begin
+(FStar_All.failwith "include not supported by legacy desugaring")
+end
 | FStar_Parser_AST.ModuleAbbrev (x, l) -> begin
 (let _157_1039 = (FStar_Parser_DesugarEnv.push_module_abbrev env x l)
 in ((_157_1039), ([])))
@@ -3645,8 +3648,8 @@ end
 | FStar_Parser_AST.Tycon (qual, tcs) -> begin
 (
 
-let tcs = (FStar_List.map (fun _62_2879 -> (match (_62_2879) with
-| (x, _62_2878) -> begin
+let tcs = (FStar_List.map (fun _62_2882 -> (match (_62_2882) with
+| (x, _62_2881) -> begin
 x
 end)) tcs)
 in (let _157_1041 = (trans_quals qual)
@@ -3656,28 +3659,28 @@ end
 (match ((let _157_1043 = (let _157_1042 = (desugar_exp_maybe_top true env (FStar_Parser_AST.mk_term (FStar_Parser_AST.Let (((isrec), (lets), ((FStar_Parser_AST.mk_term (FStar_Parser_AST.Const (FStar_Const.Const_unit)) d.FStar_Parser_AST.drange FStar_Parser_AST.Expr))))) d.FStar_Parser_AST.drange FStar_Parser_AST.Expr))
 in (FStar_All.pipe_left FStar_Absyn_Util.compress_exp _157_1042))
 in _157_1043.FStar_Absyn_Syntax.n)) with
-| FStar_Absyn_Syntax.Exp_let (lbs, _62_2888) -> begin
+| FStar_Absyn_Syntax.Exp_let (lbs, _62_2891) -> begin
 (
 
 let lids = (FStar_All.pipe_right (Prims.snd lbs) (FStar_List.map (fun lb -> (match (lb.FStar_Absyn_Syntax.lbname) with
 | FStar_Util.Inr (l) -> begin
 l
 end
-| _62_2895 -> begin
+| _62_2898 -> begin
 (FStar_All.failwith "impossible")
 end))))
 in (
 
 let quals = (match (quals) with
-| (_62_2900)::_62_2898 -> begin
+| (_62_2903)::_62_2901 -> begin
 (trans_quals quals)
 end
-| _62_2903 -> begin
+| _62_2906 -> begin
 (FStar_All.pipe_right (Prims.snd lbs) (FStar_List.collect (fun _62_30 -> (match (_62_30) with
-| {FStar_Absyn_Syntax.lbname = FStar_Util.Inl (_62_2912); FStar_Absyn_Syntax.lbtyp = _62_2910; FStar_Absyn_Syntax.lbeff = _62_2908; FStar_Absyn_Syntax.lbdef = _62_2906} -> begin
+| {FStar_Absyn_Syntax.lbname = FStar_Util.Inl (_62_2915); FStar_Absyn_Syntax.lbtyp = _62_2913; FStar_Absyn_Syntax.lbeff = _62_2911; FStar_Absyn_Syntax.lbdef = _62_2909} -> begin
 []
 end
-| {FStar_Absyn_Syntax.lbname = FStar_Util.Inr (l); FStar_Absyn_Syntax.lbtyp = _62_2920; FStar_Absyn_Syntax.lbeff = _62_2918; FStar_Absyn_Syntax.lbdef = _62_2916} -> begin
+| {FStar_Absyn_Syntax.lbname = FStar_Util.Inr (l); FStar_Absyn_Syntax.lbtyp = _62_2923; FStar_Absyn_Syntax.lbeff = _62_2921; FStar_Absyn_Syntax.lbdef = _62_2919} -> begin
 (FStar_Parser_DesugarEnv.lookup_letbinding_quals env l)
 end))))
 end)
@@ -3689,7 +3692,7 @@ in (
 let env = (FStar_Parser_DesugarEnv.push_sigelt env s)
 in ((env), ((s)::[]))))))
 end
-| _62_2928 -> begin
+| _62_2931 -> begin
 (FStar_All.failwith "Desugaring a let did not produce a let")
 end)
 end
@@ -3800,8 +3803,8 @@ end
 | FStar_Parser_AST.KindAbbrev (id, binders, k) -> begin
 (
 
-let _62_2981 = (desugar_binders env binders)
-in (match (_62_2981) with
+let _62_2984 = (desugar_binders env binders)
+in (match (_62_2984) with
 | (env_k, binders) -> begin
 (
 
@@ -3818,7 +3821,7 @@ let env = (FStar_Parser_DesugarEnv.push_sigelt env se)
 in ((env), ((se)::[]))))))
 end))
 end
-| FStar_Parser_AST.NewEffectForFree (_62_2987) -> begin
+| FStar_Parser_AST.NewEffectForFree (_62_2990) -> begin
 (FStar_All.failwith "effects for free only supported in conjunction with --universes")
 end
 | FStar_Parser_AST.NewEffect (quals, FStar_Parser_AST.RedefineEffect (eff_name, eff_binders, defn)) -> begin
@@ -3827,16 +3830,16 @@ end
 let env0 = env
 in (
 
-let _62_3000 = (desugar_binders env eff_binders)
-in (match (_62_3000) with
+let _62_3003 = (desugar_binders env eff_binders)
+in (match (_62_3003) with
 | (env, binders) -> begin
 (
 
 let defn = (desugar_typ env defn)
 in (
 
-let _62_3004 = (FStar_Absyn_Util.head_and_args defn)
-in (match (_62_3004) with
+let _62_3007 = (FStar_Absyn_Util.head_and_args defn)
+in (match (_62_3007) with
 | (head, args) -> begin
 (match (head.FStar_Absyn_Syntax.n) with
 | FStar_Absyn_Syntax.Typ_const (eff) -> begin
@@ -3885,7 +3888,7 @@ let env = (FStar_Parser_DesugarEnv.push_sigelt env0 se)
 in ((env), ((se)::[])))))))
 end)
 end
-| _62_3016 -> begin
+| _62_3019 -> begin
 (let _157_1085 = (let _157_1084 = (let _157_1083 = (let _157_1082 = (FStar_Absyn_Print.typ_to_string head)
 in (Prims.strcat _157_1082 " is not an effect"))
 in ((_157_1083), (d.FStar_Parser_AST.drange)))
@@ -3904,27 +3907,27 @@ in (
 let env = (FStar_Parser_DesugarEnv.enter_monad_scope env eff_name)
 in (
 
-let _62_3031 = (desugar_binders env eff_binders)
-in (match (_62_3031) with
+let _62_3034 = (desugar_binders env eff_binders)
+in (match (_62_3034) with
 | (env, binders) -> begin
 (
 
 let eff_k = (desugar_kind env eff_kind)
 in (
 
-let _62_3042 = (FStar_All.pipe_right eff_decls (FStar_List.fold_left (fun _62_3035 decl -> (match (_62_3035) with
+let _62_3045 = (FStar_All.pipe_right eff_decls (FStar_List.fold_left (fun _62_3038 decl -> (match (_62_3038) with
 | (env, out) -> begin
 (
 
-let _62_3039 = (desugar_decl env decl)
-in (match (_62_3039) with
+let _62_3042 = (desugar_decl env decl)
+in (match (_62_3042) with
 | (env, ses) -> begin
 (let _157_1089 = (let _157_1088 = (FStar_List.hd ses)
 in (_157_1088)::out)
 in ((env), (_157_1089)))
 end))
 end)) ((env), ([]))))
-in (match (_62_3042) with
+in (match (_62_3045) with
 | (env, decls) -> begin
 (
 
@@ -3996,7 +3999,7 @@ let non_reifiable = (fun _62_31 -> (match (_62_31) with
 | FStar_Parser_AST.NonReifiableLift (f) -> begin
 f
 end
-| _62_3065 -> begin
+| _62_3068 -> begin
 (Prims.raise (FStar_Absyn_Syntax.Error ((("Unexpected reifiable sub-effect"), (d.FStar_Parser_AST.drange)))))
 end))
 in (
@@ -4010,12 +4013,12 @@ in ((env), ((se)::[]))))))))
 end)))
 
 
-let desugar_decls : FStar_Parser_DesugarEnv.env  ->  FStar_Parser_AST.decl Prims.list  ->  (FStar_Parser_DesugarEnv.env * FStar_Absyn_Syntax.sigelts) = (fun env decls -> (FStar_List.fold_left (fun _62_3073 d -> (match (_62_3073) with
+let desugar_decls : FStar_Parser_DesugarEnv.env  ->  FStar_Parser_AST.decl Prims.list  ->  (FStar_Parser_DesugarEnv.env * FStar_Absyn_Syntax.sigelts) = (fun env decls -> (FStar_List.fold_left (fun _62_3076 d -> (match (_62_3076) with
 | (env, sigelts) -> begin
 (
 
-let _62_3077 = (desugar_decl env d)
-in (match (_62_3077) with
+let _62_3080 = (desugar_decl env d)
+in (match (_62_3080) with
 | (env, se) -> begin
 ((env), ((FStar_List.append sigelts se)))
 end))
@@ -4050,7 +4053,7 @@ end
 end)
 in (
 
-let _62_3104 = (match (m) with
+let _62_3107 = (match (m) with
 | FStar_Parser_AST.Interface (mname, decls, admitted) -> begin
 (let _157_1146 = (FStar_Parser_DesugarEnv.prepare_module_or_interface true admitted env mname)
 in (let _157_1145 = (open_ns mname decls)
@@ -4061,12 +4064,12 @@ end
 in (let _157_1147 = (open_ns mname decls)
 in ((_157_1148), (mname), (_157_1147), (false))))
 end)
-in (match (_62_3104) with
+in (match (_62_3107) with
 | ((env, pop_when_done), mname, decls, intf) -> begin
 (
 
-let _62_3107 = (desugar_decls env decls)
-in (match (_62_3107) with
+let _62_3110 = (desugar_decls env decls)
+in (match (_62_3110) with
 | (env, sigelts) -> begin
 (
 
@@ -4083,7 +4086,7 @@ let m = if (FStar_Options.interactive_fsi ()) then begin
 | FStar_Parser_AST.Module (mname, decls) -> begin
 FStar_Parser_AST.Interface (((mname), (decls), (true)))
 end
-| FStar_Parser_AST.Interface (mname, _62_3118, _62_3120) -> begin
+| FStar_Parser_AST.Interface (mname, _62_3121, _62_3123) -> begin
 (FStar_All.failwith (Prims.strcat "Impossible: " mname.FStar_Ident.ident.FStar_Ident.idText))
 end)
 end else begin
@@ -4091,24 +4094,24 @@ m
 end
 in (
 
-let _62_3128 = (desugar_modul_common curmod env m)
-in (match (_62_3128) with
-| (x, y, _62_3127) -> begin
+let _62_3131 = (desugar_modul_common curmod env m)
+in (match (_62_3131) with
+| (x, y, _62_3130) -> begin
 ((x), (y))
 end))))
 
 
 let desugar_modul : FStar_Parser_DesugarEnv.env  ->  FStar_Parser_AST.modul  ->  (env_t * FStar_Absyn_Syntax.modul) = (fun env m -> (
 
-let _62_3134 = (desugar_modul_common None env m)
-in (match (_62_3134) with
+let _62_3137 = (desugar_modul_common None env m)
+in (match (_62_3137) with
 | (env, modul, pop_when_done) -> begin
 (
 
 let env = (FStar_Parser_DesugarEnv.finish_module_or_interface env modul)
 in (
 
-let _62_3136 = if (FStar_Options.dump_module modul.FStar_Absyn_Syntax.name.FStar_Ident.str) then begin
+let _62_3139 = if (FStar_Options.dump_module modul.FStar_Absyn_Syntax.name.FStar_Ident.str) then begin
 (let _157_1159 = (FStar_Absyn_Print.modul_to_string modul)
 in (FStar_Util.print1 "%s\n" _157_1159))
 end else begin
@@ -4125,17 +4128,17 @@ end)))
 
 let desugar_file : FStar_Parser_DesugarEnv.env  ->  FStar_Parser_AST.file  ->  (FStar_Parser_DesugarEnv.env * FStar_Absyn_Syntax.modul Prims.list) = (fun env f -> (
 
-let _62_3149 = (FStar_List.fold_left (fun _62_3142 m -> (match (_62_3142) with
+let _62_3152 = (FStar_List.fold_left (fun _62_3145 m -> (match (_62_3145) with
 | (env, mods) -> begin
 (
 
-let _62_3146 = (desugar_modul env m)
-in (match (_62_3146) with
+let _62_3149 = (desugar_modul env m)
+in (match (_62_3149) with
 | (env, m) -> begin
 ((env), ((m)::mods))
 end))
 end)) ((env), ([])) f)
-in (match (_62_3149) with
+in (match (_62_3152) with
 | (env, mods) -> begin
 ((env), ((FStar_List.rev mods)))
 end)))
@@ -4143,15 +4146,15 @@ end)))
 
 let add_modul_to_env : FStar_Absyn_Syntax.modul  ->  FStar_Parser_DesugarEnv.env  ->  FStar_Parser_DesugarEnv.env = (fun m en -> (
 
-let _62_3154 = (FStar_Parser_DesugarEnv.prepare_module_or_interface false false en m.FStar_Absyn_Syntax.name)
-in (match (_62_3154) with
+let _62_3157 = (FStar_Parser_DesugarEnv.prepare_module_or_interface false false en m.FStar_Absyn_Syntax.name)
+in (match (_62_3157) with
 | (en, pop_when_done) -> begin
 (
 
 let en = (FStar_List.fold_left FStar_Parser_DesugarEnv.push_sigelt (
 
-let _62_3155 = en
-in {FStar_Parser_DesugarEnv.curmodule = Some (m.FStar_Absyn_Syntax.name); FStar_Parser_DesugarEnv.modules = _62_3155.FStar_Parser_DesugarEnv.modules; FStar_Parser_DesugarEnv.open_namespaces = _62_3155.FStar_Parser_DesugarEnv.open_namespaces; FStar_Parser_DesugarEnv.modul_abbrevs = _62_3155.FStar_Parser_DesugarEnv.modul_abbrevs; FStar_Parser_DesugarEnv.sigaccum = _62_3155.FStar_Parser_DesugarEnv.sigaccum; FStar_Parser_DesugarEnv.localbindings = _62_3155.FStar_Parser_DesugarEnv.localbindings; FStar_Parser_DesugarEnv.recbindings = _62_3155.FStar_Parser_DesugarEnv.recbindings; FStar_Parser_DesugarEnv.phase = _62_3155.FStar_Parser_DesugarEnv.phase; FStar_Parser_DesugarEnv.sigmap = _62_3155.FStar_Parser_DesugarEnv.sigmap; FStar_Parser_DesugarEnv.default_result_effect = _62_3155.FStar_Parser_DesugarEnv.default_result_effect; FStar_Parser_DesugarEnv.iface = _62_3155.FStar_Parser_DesugarEnv.iface; FStar_Parser_DesugarEnv.admitted_iface = _62_3155.FStar_Parser_DesugarEnv.admitted_iface}) m.FStar_Absyn_Syntax.exports)
+let _62_3158 = en
+in {FStar_Parser_DesugarEnv.curmodule = Some (m.FStar_Absyn_Syntax.name); FStar_Parser_DesugarEnv.modules = _62_3158.FStar_Parser_DesugarEnv.modules; FStar_Parser_DesugarEnv.open_namespaces = _62_3158.FStar_Parser_DesugarEnv.open_namespaces; FStar_Parser_DesugarEnv.modul_abbrevs = _62_3158.FStar_Parser_DesugarEnv.modul_abbrevs; FStar_Parser_DesugarEnv.sigaccum = _62_3158.FStar_Parser_DesugarEnv.sigaccum; FStar_Parser_DesugarEnv.localbindings = _62_3158.FStar_Parser_DesugarEnv.localbindings; FStar_Parser_DesugarEnv.recbindings = _62_3158.FStar_Parser_DesugarEnv.recbindings; FStar_Parser_DesugarEnv.phase = _62_3158.FStar_Parser_DesugarEnv.phase; FStar_Parser_DesugarEnv.sigmap = _62_3158.FStar_Parser_DesugarEnv.sigmap; FStar_Parser_DesugarEnv.default_result_effect = _62_3158.FStar_Parser_DesugarEnv.default_result_effect; FStar_Parser_DesugarEnv.iface = _62_3158.FStar_Parser_DesugarEnv.iface; FStar_Parser_DesugarEnv.admitted_iface = _62_3158.FStar_Parser_DesugarEnv.admitted_iface}) m.FStar_Absyn_Syntax.exports)
 in (
 
 let env = (FStar_Parser_DesugarEnv.finish_module_or_interface en m)
diff --git a/src/ocaml-output/FStar_Parser_Env.ml b/src/ocaml-output/FStar_Parser_Env.ml
index 222859e580d..5b1ce6761d1 100755
--- a/src/ocaml-output/FStar_Parser_Env.ml
+++ b/src/ocaml-output/FStar_Parser_Env.ml
@@ -111,43 +111,74 @@ end))
 
 
 let ___Local_binding____0 = (fun projectee -> (match (projectee) with
-| Local_binding (_63_34) -> begin
-_63_34
+| Local_binding (_63_39) -> begin
+_63_39
 end))
 
 
 let ___Rec_binding____0 = (fun projectee -> (match (projectee) with
-| Rec_binding (_63_37) -> begin
-_63_37
+| Rec_binding (_63_42) -> begin
+_63_42
 end))
 
 
 let ___Module_abbrev____0 = (fun projectee -> (match (projectee) with
-| Module_abbrev (_63_40) -> begin
-_63_40
+| Module_abbrev (_63_45) -> begin
+_63_45
 end))
 
 
 let ___Open_module_or_namespace____0 = (fun projectee -> (match (projectee) with
-| Open_module_or_namespace (_63_43) -> begin
-_63_43
+| Open_module_or_namespace (_63_48) -> begin
+_63_48
 end))
 
 
 let ___Top_level_def____0 = (fun projectee -> (match (projectee) with
-| Top_level_def (_63_46) -> begin
-_63_46
+| Top_level_def (_63_51) -> begin
+_63_51
 end))
 
 
 let ___Record_or_dc____0 = (fun projectee -> (match (projectee) with
-| Record_or_dc (_63_49) -> begin
-_63_49
+| Record_or_dc (_63_54) -> begin
+_63_54
 end))
 
 
+type string_set =
+Prims.string FStar_Util.set
+
+
+type exported_id_kind =
+| Exported_id_term_type
+| Exported_id_field
+
+
+let is_Exported_id_term_type = (fun _discr_ -> (match (_discr_) with
+| Exported_id_term_type (_) -> begin
+true
+end
+| _ -> begin
+false
+end))
+
+
+let is_Exported_id_field = (fun _discr_ -> (match (_discr_) with
+| Exported_id_field (_) -> begin
+true
+end
+| _ -> begin
+false
+end))
+
+
+type exported_id_set =
+exported_id_kind  ->  string_set FStar_ST.ref
+
+
 type env =
-{curmodule : FStar_Ident.lident Prims.option; curmonad : FStar_Ident.ident Prims.option; modules : (FStar_Ident.lident * FStar_Syntax_Syntax.modul) Prims.list; scope_mods : scope_mod Prims.list; sigaccum : FStar_Syntax_Syntax.sigelts; sigmap : (FStar_Syntax_Syntax.sigelt * Prims.bool) FStar_Util.smap; default_result_effect : FStar_Ident.lident; iface : Prims.bool; admitted_iface : Prims.bool; expect_typ : Prims.bool}
+{curmodule : FStar_Ident.lident Prims.option; curmonad : FStar_Ident.ident Prims.option; modules : (FStar_Ident.lident * FStar_Syntax_Syntax.modul) Prims.list; scope_mods : scope_mod Prims.list; exported_ids : exported_id_set FStar_Util.smap; trans_exported_ids : exported_id_set FStar_Util.smap; includes : FStar_Ident.lident Prims.list FStar_ST.ref FStar_Util.smap; sigaccum : FStar_Syntax_Syntax.sigelts; sigmap : (FStar_Syntax_Syntax.sigelt * Prims.bool) FStar_Util.smap; default_result_effect : FStar_Ident.lident; iface : Prims.bool; admitted_iface : Prims.bool; expect_typ : Prims.bool}
 
 
 let is_Mkenv : env  ->  Prims.bool = (Obj.magic ((fun _ -> (FStar_All.failwith "Not yet implemented:is_Mkenv"))))
@@ -177,17 +208,20 @@ end))
 
 
 let ___Term_name____0 = (fun projectee -> (match (projectee) with
-| Term_name (_63_63) -> begin
-_63_63
+| Term_name (_63_71) -> begin
+_63_71
 end))
 
 
 let ___Eff_name____0 = (fun projectee -> (match (projectee) with
-| Eff_name (_63_66) -> begin
-_63_66
+| Eff_name (_63_74) -> begin
+_63_74
 end))
 
 
+let all_exported_id_kinds : exported_id_kind Prims.list = (Exported_id_field)::(Exported_id_term_type)::[]
+
+
 let open_modules : env  ->  (FStar_Ident.lident * FStar_Syntax_Syntax.modul) Prims.list = (fun e -> e.modules)
 
 
@@ -205,49 +239,52 @@ let qual : FStar_Ident.lident  ->  FStar_Ident.ident  ->  FStar_Ident.lident = F
 
 let qualify : env  ->  FStar_Ident.ident  ->  FStar_Ident.lident = (fun env id -> (match (env.curmonad) with
 | None -> begin
-(let _158_172 = (current_module env)
-in (qual _158_172 id))
+(let _158_185 = (current_module env)
+in (qual _158_185 id))
 end
 | Some (monad) -> begin
-(let _158_174 = (let _158_173 = (current_module env)
-in (qual _158_173 monad))
-in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_174 id))
+(let _158_187 = (let _158_186 = (current_module env)
+in (qual _158_186 monad))
+in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_187 id))
 end))
 
 
-let new_sigmap = (fun _63_79 -> (match (()) with
+let new_sigmap = (fun _63_87 -> (match (()) with
 | () -> begin
 (FStar_Util.smap_create (Prims.parse_int "100"))
 end))
 
 
-let empty_env : Prims.unit  ->  env = (fun _63_80 -> (match (()) with
+let empty_env : Prims.unit  ->  env = (fun _63_88 -> (match (()) with
 | () -> begin
-(let _158_178 = (new_sigmap ())
-in {curmodule = None; curmonad = None; modules = []; scope_mods = []; sigaccum = []; sigmap = _158_178; default_result_effect = FStar_Syntax_Const.effect_Tot_lid; iface = false; admitted_iface = false; expect_typ = false})
+(let _158_194 = (new_sigmap ())
+in (let _158_193 = (new_sigmap ())
+in (let _158_192 = (new_sigmap ())
+in (let _158_191 = (new_sigmap ())
+in {curmodule = None; curmonad = None; modules = []; scope_mods = []; exported_ids = _158_194; trans_exported_ids = _158_193; includes = _158_192; sigaccum = []; sigmap = _158_191; default_result_effect = FStar_Syntax_Const.effect_Tot_lid; iface = false; admitted_iface = false; expect_typ = false}))))
 end))
 
 
 let sigmap : env  ->  (FStar_Syntax_Syntax.sigelt * Prims.bool) FStar_Util.smap = (fun env -> env.sigmap)
 
 
-let has_all_in_scope : env  ->  Prims.bool = (fun env -> (FStar_List.existsb (fun _63_86 -> (match (_63_86) with
-| (m, _63_85) -> begin
+let has_all_in_scope : env  ->  Prims.bool = (fun env -> (FStar_List.existsb (fun _63_94 -> (match (_63_94) with
+| (m, _63_93) -> begin
 (FStar_Ident.lid_equals m FStar_Syntax_Const.all_lid)
 end)) env.modules))
 
 
 let default_total : env  ->  env = (fun env -> (
 
-let _63_88 = env
-in {curmodule = _63_88.curmodule; curmonad = _63_88.curmonad; modules = _63_88.modules; scope_mods = _63_88.scope_mods; sigaccum = _63_88.sigaccum; sigmap = _63_88.sigmap; default_result_effect = FStar_Syntax_Const.effect_Tot_lid; iface = _63_88.iface; admitted_iface = _63_88.admitted_iface; expect_typ = _63_88.expect_typ}))
+let _63_96 = env
+in {curmodule = _63_96.curmodule; curmonad = _63_96.curmonad; modules = _63_96.modules; scope_mods = _63_96.scope_mods; exported_ids = _63_96.exported_ids; trans_exported_ids = _63_96.trans_exported_ids; includes = _63_96.includes; sigaccum = _63_96.sigaccum; sigmap = _63_96.sigmap; default_result_effect = FStar_Syntax_Const.effect_Tot_lid; iface = _63_96.iface; admitted_iface = _63_96.admitted_iface; expect_typ = _63_96.expect_typ}))
 
 
 let default_ml : env  ->  env = (fun env -> if (has_all_in_scope env) then begin
 (
 
-let _63_91 = env
-in {curmodule = _63_91.curmodule; curmonad = _63_91.curmonad; modules = _63_91.modules; scope_mods = _63_91.scope_mods; sigaccum = _63_91.sigaccum; sigmap = _63_91.sigmap; default_result_effect = FStar_Syntax_Const.effect_ML_lid; iface = _63_91.iface; admitted_iface = _63_91.admitted_iface; expect_typ = _63_91.expect_typ})
+let _63_99 = env
+in {curmodule = _63_99.curmodule; curmonad = _63_99.curmonad; modules = _63_99.modules; scope_mods = _63_99.scope_mods; exported_ids = _63_99.exported_ids; trans_exported_ids = _63_99.trans_exported_ids; includes = _63_99.includes; sigaccum = _63_99.sigaccum; sigmap = _63_99.sigmap; default_result_effect = FStar_Syntax_Const.effect_ML_lid; iface = _63_99.iface; admitted_iface = _63_99.admitted_iface; expect_typ = _63_99.expect_typ})
 end else begin
 env
 end)
@@ -257,12 +294,12 @@ let set_bv_range : FStar_Syntax_Syntax.bv  ->  FStar_Range.range  ->  FStar_Synt
 
 let id = (
 
-let _63_95 = bv.FStar_Syntax_Syntax.ppname
-in {FStar_Ident.idText = _63_95.FStar_Ident.idText; FStar_Ident.idRange = r})
+let _63_103 = bv.FStar_Syntax_Syntax.ppname
+in {FStar_Ident.idText = _63_103.FStar_Ident.idText; FStar_Ident.idRange = r})
 in (
 
-let _63_98 = bv
-in {FStar_Syntax_Syntax.ppname = id; FStar_Syntax_Syntax.index = _63_98.FStar_Syntax_Syntax.index; FStar_Syntax_Syntax.sort = _63_98.FStar_Syntax_Syntax.sort})))
+let _63_106 = bv
+in {FStar_Syntax_Syntax.ppname = id; FStar_Syntax_Syntax.index = _63_106.FStar_Syntax_Syntax.index; FStar_Syntax_Syntax.sort = _63_106.FStar_Syntax_Syntax.sort})))
 
 
 let bv_to_name : FStar_Syntax_Syntax.bv  ->  FStar_Range.range  ->  FStar_Syntax_Syntax.term = (fun bv r -> (FStar_Syntax_Syntax.bv_to_name (set_bv_range bv r)))
@@ -273,12 +310,12 @@ let unmangleMap : (Prims.string * Prims.string * FStar_Syntax_Syntax.delta_depth
 
 let unmangleOpName : FStar_Ident.ident  ->  (FStar_Syntax_Syntax.term * Prims.bool) Prims.option = (fun id -> (
 
-let t = (FStar_Util.find_map unmangleMap (fun _63_107 -> (match (_63_107) with
+let t = (FStar_Util.find_map unmangleMap (fun _63_115 -> (match (_63_115) with
 | (x, y, dd, dq) -> begin
 if (id.FStar_Ident.idText = x) then begin
-(let _158_200 = (let _158_199 = (FStar_Ident.lid_of_path (("Prims")::(y)::[]) id.FStar_Ident.idRange)
-in (FStar_Syntax_Syntax.fvar _158_199 dd dq))
-in Some (_158_200))
+(let _158_216 = (let _158_215 = (FStar_Ident.lid_of_path (("Prims")::(y)::[]) id.FStar_Ident.idRange)
+in (FStar_Syntax_Syntax.fvar _158_215 dd dq))
+in Some (_158_216))
 end else begin
 None
 end
@@ -326,8 +363,8 @@ end))
 
 
 let ___Cont_ok____0 = (fun projectee -> (match (projectee) with
-| Cont_ok (_63_115) -> begin
-_63_115
+| Cont_ok (_63_123) -> begin
+_63_123
 end))
 
 
@@ -352,8 +389,8 @@ let constrname = record.constrname.FStar_Ident.ident
 in (
 
 let fname = if needs_constrname then begin
-(let _158_231 = (FStar_Ident.lid_of_ids (FStar_List.append ns ((constrname)::[])))
-in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_231 id))
+(let _158_247 = (FStar_Ident.lid_of_ids (FStar_List.append ns ((constrname)::[])))
+in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_247 id))
 end else begin
 (FStar_Ident.lid_of_ids (FStar_List.append ns ((id)::[])))
 end
@@ -362,8 +399,8 @@ in (
 let fname = (FStar_Ident.set_lid_range fname id.FStar_Ident.idRange)
 in (
 
-let find = (FStar_Util.find_map record.fields (fun _63_134 -> (match (_63_134) with
-| (f, _63_133) -> begin
+let find = (FStar_Util.find_map record.fields (fun _63_142 -> (match (_63_142) with
+| (f, _63_141) -> begin
 if (FStar_Ident.lid_equals fname f) then begin
 Some (((record), (fname)))
 end else begin
@@ -379,64 +416,143 @@ Cont_ignore
 end)))))))
 
 
-let try_lookup_id'' = (fun env id k_local_binding k_rec_binding k_record find_in_module lookup_default_id -> (
+let get_exported_id_set : env  ->  Prims.string  ->  (exported_id_kind  ->  string_set FStar_ST.ref) Prims.option = (fun e mname -> (FStar_Util.smap_try_find e.exported_ids mname))
+
+
+let get_trans_exported_id_set : env  ->  Prims.string  ->  (exported_id_kind  ->  string_set FStar_ST.ref) Prims.option = (fun e mname -> (FStar_Util.smap_try_find e.trans_exported_ids mname))
+
+
+let string_of_exported_id_kind : exported_id_kind  ->  Prims.string = (fun _63_2 -> (match (_63_2) with
+| Exported_id_field -> begin
+"field"
+end
+| Exported_id_term_type -> begin
+"term/type"
+end))
+
+
+let find_in_module_with_includes = (fun eikind find_in_module find_in_module_default env ns id -> (
 
-let check_local_binding_id = (fun _63_2 -> (match (_63_2) with
-| (id', _63_150, _63_152) -> begin
+let idstr = id.FStar_Ident.idText
+in (
+
+let rec aux = (fun _63_3 -> (match (_63_3) with
+| [] -> begin
+find_in_module_default
+end
+| (modul)::q -> begin
+(
+
+let mname = modul.FStar_Ident.str
+in (
+
+let not_shadowed = (match ((get_exported_id_set env mname)) with
+| None -> begin
+true
+end
+| Some (mex) -> begin
+(
+
+let mexports = (let _158_287 = (mex eikind)
+in (FStar_ST.read _158_287))
+in (FStar_Util.set_mem idstr mexports))
+end)
+in (
+
+let mincludes = (match ((FStar_Util.smap_try_find env.includes mname)) with
+| None -> begin
+[]
+end
+| Some (minc) -> begin
+(FStar_ST.read minc)
+end)
+in (
+
+let look_into = if not_shadowed then begin
+(let _158_288 = (qual modul id)
+in (find_in_module _158_288))
+end else begin
+Cont_ignore
+end
+in (match (look_into) with
+| Cont_ignore -> begin
+(aux (FStar_List.append mincludes q))
+end
+| _63_181 -> begin
+look_into
+end)))))
+end))
+in (aux ((ns)::[])))))
+
+
+let is_exported_id_field : exported_id_kind  ->  Prims.bool = (fun _63_4 -> (match (_63_4) with
+| Exported_id_field -> begin
+true
+end
+| _63_185 -> begin
+false
+end))
+
+
+let try_lookup_id'' = (fun env id eikind k_local_binding k_rec_binding k_record find_in_module lookup_default_id -> (
+
+let check_local_binding_id = (fun _63_5 -> (match (_63_5) with
+| (id', _63_198, _63_200) -> begin
 (id'.FStar_Ident.idText = id.FStar_Ident.idText)
 end))
 in (
 
-let check_rec_binding_id = (fun _63_3 -> (match (_63_3) with
-| (id', _63_158, _63_160) -> begin
+let check_rec_binding_id = (fun _63_6 -> (match (_63_6) with
+| (id', _63_206, _63_208) -> begin
 (id'.FStar_Ident.idText = id.FStar_Ident.idText)
 end))
 in (
 
-let curmod_ns = (let _158_262 = (current_module env)
-in (FStar_Ident.ids_of_lid _158_262))
+let curmod_ns = (let _158_321 = (current_module env)
+in (FStar_Ident.ids_of_lid _158_321))
 in (
 
-let proc = (fun _63_4 -> (match (_63_4) with
+let proc = (fun _63_7 -> (match (_63_7) with
 | Local_binding (l) when (check_local_binding_id l) -> begin
 (k_local_binding l)
 end
 | Rec_binding (r) when (check_rec_binding_id r) -> begin
 (k_rec_binding r)
 end
-| Open_module_or_namespace (ns, _63_171) -> begin
-(
-
-let lid = (qual ns id)
-in (find_in_module lid))
+| Open_module_or_namespace (ns, _63_219) -> begin
+(find_in_module_with_includes eikind find_in_module Cont_ignore env ns id)
 end
 | Top_level_def (id') when (id'.FStar_Ident.idText = id.FStar_Ident.idText) -> begin
 (lookup_default_id Cont_ignore id)
 end
-| Record_or_dc (r) -> begin
-(find_in_record curmod_ns id r k_record)
+| Record_or_dc (r) when (is_exported_id_field eikind) -> begin
+(let _158_325 = (FStar_Ident.lid_of_ids curmod_ns)
+in (find_in_module_with_includes Exported_id_field (fun lid -> (
+
+let id = lid.FStar_Ident.ident
+in (find_in_record lid.FStar_Ident.ns id r k_record))) Cont_ignore env _158_325 id))
 end
-| _63_180 -> begin
+| _63_229 -> begin
 Cont_ignore
 end))
 in (
 
-let rec aux = (fun _63_5 -> (match (_63_5) with
+let rec aux = (fun _63_8 -> (match (_63_8) with
 | (a)::q -> begin
-(let _158_268 = (proc a)
-in (option_of_cont (fun _63_187 -> (aux q)) _158_268))
+(let _158_329 = (proc a)
+in (option_of_cont (fun _63_236 -> (aux q)) _158_329))
 end
 | [] -> begin
-(let _158_270 = (lookup_default_id Cont_fail id)
-in (option_of_cont (fun _63_190 -> None) _158_270))
+(let _158_331 = (lookup_default_id Cont_fail id)
+in (option_of_cont (fun _63_239 -> None) _158_331))
 end))
 in (aux env.scope_mods)))))))
 
 
-let found_local_binding = (fun _63_195 -> (match (_63_195) with
+let found_local_binding = (fun _63_244 -> (match (_63_244) with
 | (id', x, mut) -> begin
-(let _158_272 = (bv_to_name x id'.FStar_Ident.idRange)
-in ((_158_272), (mut)))
+(let _158_333 = (bv_to_name x id'.FStar_Ident.idRange)
+in ((_158_333), (mut)))
 end))
 
 
@@ -453,23 +569,23 @@ let try_lookup_id : env  ->  FStar_Ident.ident  ->  (FStar_Syntax_Syntax.term *
 | Some (f) -> begin
 Some (f)
 end
-| _63_208 -> begin
-(try_lookup_id'' env id (fun r -> (let _158_288 = (found_local_binding r)
-in Cont_ok (_158_288))) (fun _63_220 -> Cont_fail) (fun _63_218 -> Cont_ignore) (fun i -> (find_in_module env i (fun _63_214 _63_216 -> Cont_fail) Cont_ignore)) (fun _63_209 _63_211 -> Cont_fail))
+| _63_257 -> begin
+(try_lookup_id'' env id Exported_id_term_type (fun r -> (let _158_349 = (found_local_binding r)
+in Cont_ok (_158_349))) (fun _63_269 -> Cont_fail) (fun _63_267 -> Cont_ignore) (fun i -> (find_in_module env i (fun _63_263 _63_265 -> Cont_fail) Cont_ignore)) (fun _63_258 _63_260 -> Cont_fail))
 end))
 
 
 let lookup_default_id = (fun env id k_global_def k_not_found -> (
 
 let find_in_monad = (match (env.curmonad) with
-| Some (_63_229) -> begin
+| Some (_63_278) -> begin
 (
 
 let lid = (qualify env id)
 in (match ((FStar_Util.smap_try_find (sigmap env) lid.FStar_Ident.str)) with
 | Some (r) -> begin
-(let _158_306 = (k_global_def lid r)
-in Some (_158_306))
+(let _158_367 = (k_global_def lid r)
+in Some (_158_367))
 end
 | None -> begin
 None
@@ -485,14 +601,14 @@ end
 | None -> begin
 (
 
-let lid = (let _158_307 = (current_module env)
-in (qual _158_307 id))
+let lid = (let _158_368 = (current_module env)
+in (qual _158_368 id))
 in (find_in_module env lid k_global_def k_not_found))
 end)))
 
 
-let module_is_defined : env  ->  FStar_Ident.lident  ->  Prims.bool = (fun env lid -> ((let _158_312 = (current_module env)
-in (FStar_Ident.lid_equals lid _158_312)) || (FStar_List.existsb (fun x -> (FStar_Ident.lid_equals lid (Prims.fst x))) env.modules)))
+let module_is_defined : env  ->  FStar_Ident.lident  ->  Prims.bool = (fun env lid -> ((let _158_373 = (current_module env)
+in (FStar_Ident.lid_equals lid _158_373)) || (FStar_List.existsb (fun x -> (FStar_Ident.lid_equals lid (Prims.fst x))) env.modules)))
 
 
 let resolve_module_name : env  ->  FStar_Ident.lident  ->  Prims.bool  ->  FStar_Ident.lident Prims.option = (fun env lid honor_ns -> (
@@ -500,7 +616,7 @@ let resolve_module_name : env  ->  FStar_Ident.lident  ->  Prims.bool  ->  FStar
 let nslen = (FStar_List.length lid.FStar_Ident.ns)
 in (
 
-let rec aux = (fun _63_6 -> (match (_63_6) with
+let rec aux = (fun _63_9 -> (match (_63_9) with
 | [] -> begin
 if (module_is_defined env lid) then begin
 Some (lid)
@@ -511,47 +627,44 @@ end
 | (Open_module_or_namespace (ns, Open_namespace))::q when honor_ns -> begin
 (
 
-let new_lid = (let _158_324 = (let _158_323 = (FStar_Ident.path_of_lid ns)
-in (let _158_322 = (FStar_Ident.path_of_lid lid)
-in (FStar_List.append _158_323 _158_322)))
-in (FStar_Ident.lid_of_path _158_324 (FStar_Ident.range_of_lid lid)))
+let new_lid = (let _158_385 = (let _158_384 = (FStar_Ident.path_of_lid ns)
+in (let _158_383 = (FStar_Ident.path_of_lid lid)
+in (FStar_List.append _158_384 _158_383)))
+in (FStar_Ident.lid_of_path _158_385 (FStar_Ident.range_of_lid lid)))
 in if (module_is_defined env new_lid) then begin
 Some (new_lid)
 end else begin
 (aux q)
 end)
 end
-| (Module_abbrev (name, modul))::_63_259 when ((nslen = (Prims.parse_int "0")) && (name.FStar_Ident.idText = lid.FStar_Ident.ident.FStar_Ident.idText)) -> begin
+| (Module_abbrev (name, modul))::_63_308 when ((nslen = (Prims.parse_int "0")) && (name.FStar_Ident.idText = lid.FStar_Ident.ident.FStar_Ident.idText)) -> begin
 Some (modul)
 end
-| (_63_267)::q -> begin
+| (_63_316)::q -> begin
 (aux q)
 end))
 in (aux env.scope_mods))))
 
 
-let resolve_in_open_namespaces'' = (fun env lid k_local_binding k_rec_binding k_record f_module l_default -> (match (lid.FStar_Ident.ns) with
-| (_63_280)::_63_278 -> begin
-(match ((let _158_354 = (let _158_353 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
-in (FStar_Ident.set_lid_range _158_353 (FStar_Ident.range_of_lid lid)))
-in (resolve_module_name env _158_354 true))) with
+let resolve_in_open_namespaces'' = (fun env lid eikind k_local_binding k_rec_binding k_record f_module l_default -> (match (lid.FStar_Ident.ns) with
+| (_63_330)::_63_328 -> begin
+(match ((let _158_413 = (let _158_412 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
+in (FStar_Ident.set_lid_range _158_412 (FStar_Ident.range_of_lid lid)))
+in (resolve_module_name env _158_413 true))) with
 | None -> begin
 None
 end
 | Some (modul) -> begin
-(
-
-let lid' = (qual modul lid.FStar_Ident.ident)
-in (let _158_356 = (f_module Cont_fail lid')
-in (option_of_cont (fun _63_286 -> None) _158_356)))
+(let _158_415 = (find_in_module_with_includes eikind f_module Cont_fail env modul lid.FStar_Ident.ident)
+in (option_of_cont (fun _63_335 -> None) _158_415))
 end)
 end
 | [] -> begin
-(try_lookup_id'' env lid.FStar_Ident.ident k_local_binding k_rec_binding k_record (f_module Cont_ignore) l_default)
+(try_lookup_id'' env lid.FStar_Ident.ident eikind k_local_binding k_rec_binding k_record f_module l_default)
 end))
 
 
-let cont_of_option = (fun k_none _63_7 -> (match (_63_7) with
+let cont_of_option = (fun k_none _63_10 -> (match (_63_10) with
 | Some (v) -> begin
 Cont_ok (v)
 end
@@ -562,28 +675,31 @@ end))
 
 let resolve_in_open_namespaces' = (fun env lid k_local_binding k_rec_binding k_global_def -> (
 
-let k_global_def' = (fun k lid def -> (let _158_382 = (k_global_def lid def)
-in (cont_of_option k _158_382)))
+let k_global_def' = (fun k lid def -> (let _158_441 = (k_global_def lid def)
+in (cont_of_option k _158_441)))
 in (
 
-let f_module = (fun k lid' -> (find_in_module env lid' (k_global_def' k) k))
+let f_module = (fun lid' -> (
+
+let k = Cont_ignore
+in (find_in_module env lid' (k_global_def' k) k)))
 in (
 
 let l_default = (fun k i -> (lookup_default_id env i (k_global_def' k) k))
-in (resolve_in_open_namespaces'' env lid (fun l -> (let _158_392 = (k_local_binding l)
-in (cont_of_option Cont_fail _158_392))) (fun r -> (let _158_394 = (k_rec_binding r)
-in (cont_of_option Cont_fail _158_394))) (fun _63_311 -> Cont_ignore) f_module l_default)))))
+in (resolve_in_open_namespaces'' env lid Exported_id_term_type (fun l -> (let _158_449 = (k_local_binding l)
+in (cont_of_option Cont_fail _158_449))) (fun r -> (let _158_451 = (k_rec_binding r)
+in (cont_of_option Cont_fail _158_451))) (fun _63_360 -> Cont_ignore) f_module l_default)))))
 
 
-let fv_qual_of_se : FStar_Syntax_Syntax.sigelt  ->  FStar_Syntax_Syntax.fv_qual Prims.option = (fun _63_9 -> (match (_63_9) with
-| FStar_Syntax_Syntax.Sig_datacon (_63_317, _63_319, _63_321, l, _63_324, quals, _63_327, _63_329) -> begin
+let fv_qual_of_se : FStar_Syntax_Syntax.sigelt  ->  FStar_Syntax_Syntax.fv_qual Prims.option = (fun _63_12 -> (match (_63_12) with
+| FStar_Syntax_Syntax.Sig_datacon (_63_366, _63_368, _63_370, l, _63_373, quals, _63_376, _63_378) -> begin
 (
 
-let qopt = (FStar_Util.find_map quals (fun _63_8 -> (match (_63_8) with
+let qopt = (FStar_Util.find_map quals (fun _63_11 -> (match (_63_11) with
 | FStar_Syntax_Syntax.RecordConstructor (fs) -> begin
 Some (FStar_Syntax_Syntax.Record_ctor (((l), (fs))))
 end
-| _63_336 -> begin
+| _63_385 -> begin
 None
 end)))
 in (match (qopt) with
@@ -594,15 +710,15 @@ end
 x
 end))
 end
-| FStar_Syntax_Syntax.Sig_declare_typ (_63_341, _63_343, _63_345, quals, _63_348) -> begin
+| FStar_Syntax_Syntax.Sig_declare_typ (_63_390, _63_392, _63_394, quals, _63_397) -> begin
 None
 end
-| _63_352 -> begin
+| _63_401 -> begin
 None
 end))
 
 
-let lb_fv : FStar_Syntax_Syntax.letbinding Prims.list  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.fv = (fun lbs lid -> (let _158_404 = (FStar_Util.find_map lbs (fun lb -> (
+let lb_fv : FStar_Syntax_Syntax.letbinding Prims.list  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.fv = (fun lbs lid -> (let _158_461 = (FStar_Util.find_map lbs (fun lb -> (
 
 let fv = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
 in if (FStar_Syntax_Syntax.fv_eq_lid fv lid) then begin
@@ -610,11 +726,11 @@ Some (fv)
 end else begin
 None
 end)))
-in (FStar_All.pipe_right _158_404 FStar_Util.must)))
+in (FStar_All.pipe_right _158_461 FStar_Util.must)))
 
 
-let ns_of_lid_equals : FStar_Ident.lident  ->  FStar_Ident.lident  ->  Prims.bool = (fun lid ns -> (((FStar_List.length lid.FStar_Ident.ns) = (FStar_List.length (FStar_Ident.ids_of_lid ns))) && (let _158_409 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
-in (FStar_Ident.lid_equals _158_409 ns))))
+let ns_of_lid_equals : FStar_Ident.lident  ->  FStar_Ident.lident  ->  Prims.bool = (fun lid ns -> (((FStar_List.length lid.FStar_Ident.ns) = (FStar_List.length (FStar_Ident.ids_of_lid ns))) && (let _158_466 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
+in (FStar_Ident.lid_equals _158_466 ns))))
 
 
 let try_lookup_name : Prims.bool  ->  Prims.bool  ->  env  ->  FStar_Ident.lident  ->  foundname Prims.option = (fun any_val exclude_interf env lid -> (
@@ -622,40 +738,40 @@ let try_lookup_name : Prims.bool  ->  Prims.bool  ->  env  ->  FStar_Ident.liden
 let occurrence_range = (FStar_Ident.range_of_lid lid)
 in (
 
-let k_global_def = (fun source_lid _63_13 -> (match (_63_13) with
-| (_63_368, true) when exclude_interf -> begin
+let k_global_def = (fun source_lid _63_16 -> (match (_63_16) with
+| (_63_417, true) when exclude_interf -> begin
 None
 end
-| (se, _63_373) -> begin
+| (se, _63_422) -> begin
 (match (se) with
-| FStar_Syntax_Syntax.Sig_inductive_typ (_63_376) -> begin
-(let _158_424 = (let _158_423 = (let _158_422 = (FStar_Syntax_Syntax.fvar source_lid FStar_Syntax_Syntax.Delta_constant None)
-in ((_158_422), (false)))
-in Term_name (_158_423))
-in Some (_158_424))
-end
-| FStar_Syntax_Syntax.Sig_datacon (_63_379) -> begin
-(let _158_428 = (let _158_427 = (let _158_426 = (let _158_425 = (fv_qual_of_se se)
-in (FStar_Syntax_Syntax.fvar source_lid FStar_Syntax_Syntax.Delta_constant _158_425))
-in ((_158_426), (false)))
-in Term_name (_158_427))
-in Some (_158_428))
-end
-| FStar_Syntax_Syntax.Sig_let ((_63_382, lbs), _63_386, _63_388, _63_390) -> begin
+| FStar_Syntax_Syntax.Sig_inductive_typ (_63_425) -> begin
+(let _158_481 = (let _158_480 = (let _158_479 = (FStar_Syntax_Syntax.fvar source_lid FStar_Syntax_Syntax.Delta_constant None)
+in ((_158_479), (false)))
+in Term_name (_158_480))
+in Some (_158_481))
+end
+| FStar_Syntax_Syntax.Sig_datacon (_63_428) -> begin
+(let _158_485 = (let _158_484 = (let _158_483 = (let _158_482 = (fv_qual_of_se se)
+in (FStar_Syntax_Syntax.fvar source_lid FStar_Syntax_Syntax.Delta_constant _158_482))
+in ((_158_483), (false)))
+in Term_name (_158_484))
+in Some (_158_485))
+end
+| FStar_Syntax_Syntax.Sig_let ((_63_431, lbs), _63_435, _63_437, _63_439) -> begin
 (
 
 let fv = (lb_fv lbs source_lid)
-in (let _158_431 = (let _158_430 = (let _158_429 = (FStar_Syntax_Syntax.fvar source_lid fv.FStar_Syntax_Syntax.fv_delta fv.FStar_Syntax_Syntax.fv_qual)
-in ((_158_429), (false)))
-in Term_name (_158_430))
-in Some (_158_431)))
+in (let _158_488 = (let _158_487 = (let _158_486 = (FStar_Syntax_Syntax.fvar source_lid fv.FStar_Syntax_Syntax.fv_delta fv.FStar_Syntax_Syntax.fv_qual)
+in ((_158_486), (false)))
+in Term_name (_158_487))
+in Some (_158_488)))
 end
-| FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_396, _63_398, quals, _63_401) -> begin
-if (any_val || (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_10 -> (match (_63_10) with
+| FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_445, _63_447, quals, _63_450) -> begin
+if (any_val || (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_13 -> (match (_63_13) with
 | FStar_Syntax_Syntax.Assumption -> begin
 true
 end
-| _63_407 -> begin
+| _63_456 -> begin
 false
 end))))) then begin
 (
@@ -663,22 +779,22 @@ end))))) then begin
 let lid = (FStar_Ident.set_lid_range lid (FStar_Ident.range_of_lid source_lid))
 in (
 
-let dd = if ((FStar_Syntax_Util.is_primop_lid lid) || ((ns_of_lid_equals lid FStar_Syntax_Const.prims_lid) && (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_11 -> (match (_63_11) with
+let dd = if ((FStar_Syntax_Util.is_primop_lid lid) || ((ns_of_lid_equals lid FStar_Syntax_Const.prims_lid) && (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_14 -> (match (_63_14) with
 | (FStar_Syntax_Syntax.Projector (_)) | (FStar_Syntax_Syntax.Discriminator (_)) -> begin
 true
 end
-| _63_417 -> begin
+| _63_466 -> begin
 false
 end)))))) then begin
 FStar_Syntax_Syntax.Delta_equational
 end else begin
 FStar_Syntax_Syntax.Delta_constant
 end
-in (match ((FStar_Util.find_map quals (fun _63_12 -> (match (_63_12) with
+in (match ((FStar_Util.find_map quals (fun _63_15 -> (match (_63_15) with
 | FStar_Syntax_Syntax.Reflectable (refl_monad) -> begin
 Some (refl_monad)
 end
-| _63_423 -> begin
+| _63_472 -> begin
 None
 end)))) with
 | Some (refl_monad) -> begin
@@ -687,12 +803,12 @@ end)))) with
 let refl_const = (FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_reflect (refl_monad))) None occurrence_range)
 in Some (Term_name (((refl_const), (false)))))
 end
-| _63_428 -> begin
-(let _158_438 = (let _158_437 = (let _158_436 = (let _158_435 = (fv_qual_of_se se)
-in (FStar_Syntax_Syntax.fvar lid dd _158_435))
-in ((_158_436), (false)))
-in Term_name (_158_437))
-in Some (_158_438))
+| _63_477 -> begin
+(let _158_495 = (let _158_494 = (let _158_493 = (let _158_492 = (fv_qual_of_se se)
+in (FStar_Syntax_Syntax.fvar lid dd _158_492))
+in ((_158_493), (false)))
+in Term_name (_158_494))
+in Some (_158_495))
 end)))
 end else begin
 None
@@ -701,26 +817,26 @@ end
 | (FStar_Syntax_Syntax.Sig_new_effect_for_free (ne, _)) | (FStar_Syntax_Syntax.Sig_new_effect (ne, _)) -> begin
 Some (Eff_name (((se), ((FStar_Ident.set_lid_range ne.FStar_Syntax_Syntax.mname (FStar_Ident.range_of_lid source_lid))))))
 end
-| FStar_Syntax_Syntax.Sig_effect_abbrev (_63_439) -> begin
+| FStar_Syntax_Syntax.Sig_effect_abbrev (_63_488) -> begin
 Some (Eff_name (((se), (source_lid))))
 end
-| _63_442 -> begin
+| _63_491 -> begin
 None
 end)
 end))
 in (
 
-let k_local_binding = (fun r -> (let _158_442 = (let _158_441 = (found_local_binding r)
-in Term_name (_158_441))
-in Some (_158_442)))
+let k_local_binding = (fun r -> (let _158_499 = (let _158_498 = (found_local_binding r)
+in Term_name (_158_498))
+in Some (_158_499)))
 in (
 
-let k_rec_binding = (fun _63_449 -> (match (_63_449) with
+let k_rec_binding = (fun _63_498 -> (match (_63_498) with
 | (id, l, dd) -> begin
-(let _158_447 = (let _158_446 = (let _158_445 = (FStar_Syntax_Syntax.fvar (FStar_Ident.set_lid_range l (FStar_Ident.range_of_lid lid)) dd None)
-in ((_158_445), (false)))
-in Term_name (_158_446))
-in Some (_158_447))
+(let _158_504 = (let _158_503 = (let _158_502 = (FStar_Syntax_Syntax.fvar (FStar_Ident.set_lid_range l (FStar_Ident.range_of_lid lid)) dd None)
+in ((_158_502), (false)))
+in Term_name (_158_503))
+in Some (_158_504))
 end))
 in (
 
@@ -730,11 +846,11 @@ let found_unmangled = (match (lid.FStar_Ident.ns) with
 | Some (f) -> begin
 Some (Term_name (f))
 end
-| _63_454 -> begin
+| _63_503 -> begin
 None
 end)
 end
-| _63_456 -> begin
+| _63_505 -> begin
 None
 end)
 in (match (found_unmangled) with
@@ -750,7 +866,7 @@ let try_lookup_effect_name' : Prims.bool  ->  env  ->  FStar_Ident.lident  ->  (
 | Some (Eff_name (o, l)) -> begin
 Some (((o), (l)))
 end
-| _63_469 -> begin
+| _63_518 -> begin
 None
 end))
 
@@ -759,19 +875,19 @@ let try_lookup_effect_name : env  ->  FStar_Ident.lident  ->  FStar_Ident.lident
 | Some (o, l) -> begin
 Some (l)
 end
-| _63_477 -> begin
+| _63_526 -> begin
 None
 end))
 
 
 let try_lookup_effect_defn : env  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.eff_decl Prims.option = (fun env l -> (match ((try_lookup_effect_name' (not (env.iface)) env l)) with
-| Some (FStar_Syntax_Syntax.Sig_new_effect (ne, _63_482), _63_486) -> begin
+| Some (FStar_Syntax_Syntax.Sig_new_effect (ne, _63_531), _63_535) -> begin
 Some (ne)
 end
-| Some (FStar_Syntax_Syntax.Sig_new_effect_for_free (ne, _63_491), _63_495) -> begin
+| Some (FStar_Syntax_Syntax.Sig_new_effect_for_free (ne, _63_540), _63_544) -> begin
 Some (ne)
 end
-| _63_499 -> begin
+| _63_548 -> begin
 None
 end))
 
@@ -780,34 +896,34 @@ let is_effect_name : env  ->  FStar_Ident.lident  ->  Prims.bool = (fun env lid
 | None -> begin
 false
 end
-| Some (_63_504) -> begin
+| Some (_63_553) -> begin
 true
 end))
 
 
 let lookup_letbinding_quals : env  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.qualifier Prims.list = (fun env lid -> (
 
-let k_global_def = (fun lid _63_14 -> (match (_63_14) with
-| (FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_513, _63_515, quals, _63_518), _63_522) -> begin
+let k_global_def = (fun lid _63_17 -> (match (_63_17) with
+| (FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_562, _63_564, quals, _63_567), _63_571) -> begin
 Some (quals)
 end
-| _63_525 -> begin
+| _63_574 -> begin
 None
 end))
-in (match ((resolve_in_open_namespaces' env lid (fun _63_528 -> None) (fun _63_526 -> None) k_global_def)) with
+in (match ((resolve_in_open_namespaces' env lid (fun _63_577 -> None) (fun _63_575 -> None) k_global_def)) with
 | Some (quals) -> begin
 quals
 end
-| _63_533 -> begin
+| _63_582 -> begin
 []
 end)))
 
 
-let try_lookup_module : env  ->  Prims.string Prims.list  ->  FStar_Syntax_Syntax.modul Prims.option = (fun env path -> (match ((FStar_List.tryFind (fun _63_538 -> (match (_63_538) with
+let try_lookup_module : env  ->  Prims.string Prims.list  ->  FStar_Syntax_Syntax.modul Prims.option = (fun env path -> (match ((FStar_List.tryFind (fun _63_587 -> (match (_63_587) with
 | (mlid, modul) -> begin
 ((FStar_Ident.path_of_lid mlid) = path)
 end)) env.modules)) with
-| Some (_63_540, modul) -> begin
+| Some (_63_589, modul) -> begin
 Some (modul)
 end
 | None -> begin
@@ -817,43 +933,43 @@ end))
 
 let try_lookup_let : env  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.term Prims.option = (fun env lid -> (
 
-let k_global_def = (fun lid _63_15 -> (match (_63_15) with
-| (FStar_Syntax_Syntax.Sig_let ((_63_551, lbs), _63_555, _63_557, _63_559), _63_563) -> begin
+let k_global_def = (fun lid _63_18 -> (match (_63_18) with
+| (FStar_Syntax_Syntax.Sig_let ((_63_600, lbs), _63_604, _63_606, _63_608), _63_612) -> begin
 (
 
 let fv = (lb_fv lbs lid)
-in (let _158_489 = (FStar_Syntax_Syntax.fvar lid fv.FStar_Syntax_Syntax.fv_delta fv.FStar_Syntax_Syntax.fv_qual)
-in Some (_158_489)))
+in (let _158_546 = (FStar_Syntax_Syntax.fvar lid fv.FStar_Syntax_Syntax.fv_delta fv.FStar_Syntax_Syntax.fv_qual)
+in Some (_158_546)))
 end
-| _63_567 -> begin
+| _63_616 -> begin
 None
 end))
-in (resolve_in_open_namespaces' env lid (fun _63_570 -> None) (fun _63_568 -> None) k_global_def)))
+in (resolve_in_open_namespaces' env lid (fun _63_619 -> None) (fun _63_617 -> None) k_global_def)))
 
 
 let try_lookup_definition : env  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.term Prims.option = (fun env lid -> (
 
-let k_global_def = (fun lid _63_16 -> (match (_63_16) with
-| (FStar_Syntax_Syntax.Sig_let (lbs, _63_579, _63_581, _63_583), _63_587) -> begin
+let k_global_def = (fun lid _63_19 -> (match (_63_19) with
+| (FStar_Syntax_Syntax.Sig_let (lbs, _63_628, _63_630, _63_632), _63_636) -> begin
 (FStar_Util.find_map (Prims.snd lbs) (fun lb -> (match (lb.FStar_Syntax_Syntax.lbname) with
 | FStar_Util.Inr (fv) when (FStar_Syntax_Syntax.fv_eq_lid fv lid) -> begin
 Some (lb.FStar_Syntax_Syntax.lbdef)
 end
-| _63_593 -> begin
+| _63_642 -> begin
 None
 end)))
 end
-| _63_595 -> begin
+| _63_644 -> begin
 None
 end))
-in (resolve_in_open_namespaces' env lid (fun _63_598 -> None) (fun _63_596 -> None) k_global_def)))
+in (resolve_in_open_namespaces' env lid (fun _63_647 -> None) (fun _63_645 -> None) k_global_def)))
 
 
 let try_lookup_lid' : Prims.bool  ->  Prims.bool  ->  env  ->  FStar_Ident.lident  ->  (FStar_Syntax_Syntax.term * Prims.bool) Prims.option = (fun any_val exclude_interf env lid -> (match ((try_lookup_name any_val exclude_interf env lid)) with
 | Some (Term_name (e, mut)) -> begin
 Some (((e), (mut)))
 end
-| _63_610 -> begin
+| _63_659 -> begin
 None
 end))
 
@@ -863,41 +979,41 @@ let try_lookup_lid : env  ->  FStar_Ident.lident  ->  (FStar_Syntax_Syntax.term
 
 let try_lookup_datacon : env  ->  FStar_Ident.lident  ->  FStar_Syntax_Syntax.fv Prims.option = (fun env lid -> (
 
-let k_global_def = (fun lid _63_18 -> (match (_63_18) with
-| (FStar_Syntax_Syntax.Sig_declare_typ (_63_619, _63_621, _63_623, quals, _63_626), _63_630) -> begin
-if (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_17 -> (match (_63_17) with
+let k_global_def = (fun lid _63_21 -> (match (_63_21) with
+| (FStar_Syntax_Syntax.Sig_declare_typ (_63_668, _63_670, _63_672, quals, _63_675), _63_679) -> begin
+if (FStar_All.pipe_right quals (FStar_Util.for_some (fun _63_20 -> (match (_63_20) with
 | FStar_Syntax_Syntax.Assumption -> begin
 true
 end
-| _63_635 -> begin
+| _63_684 -> begin
 false
 end)))) then begin
-(let _158_524 = (FStar_Syntax_Syntax.lid_as_fv lid FStar_Syntax_Syntax.Delta_constant None)
-in Some (_158_524))
+(let _158_581 = (FStar_Syntax_Syntax.lid_as_fv lid FStar_Syntax_Syntax.Delta_constant None)
+in Some (_158_581))
 end else begin
 None
 end
 end
-| (FStar_Syntax_Syntax.Sig_datacon (_63_637), _63_640) -> begin
-(let _158_525 = (FStar_Syntax_Syntax.lid_as_fv lid FStar_Syntax_Syntax.Delta_constant (Some (FStar_Syntax_Syntax.Data_ctor)))
-in Some (_158_525))
+| (FStar_Syntax_Syntax.Sig_datacon (_63_686), _63_689) -> begin
+(let _158_582 = (FStar_Syntax_Syntax.lid_as_fv lid FStar_Syntax_Syntax.Delta_constant (Some (FStar_Syntax_Syntax.Data_ctor)))
+in Some (_158_582))
 end
-| _63_643 -> begin
+| _63_692 -> begin
 None
 end))
-in (resolve_in_open_namespaces' env lid (fun _63_646 -> None) (fun _63_644 -> None) k_global_def)))
+in (resolve_in_open_namespaces' env lid (fun _63_695 -> None) (fun _63_693 -> None) k_global_def)))
 
 
 let find_all_datacons : env  ->  FStar_Ident.lident  ->  FStar_Ident.lident Prims.list Prims.option = (fun env lid -> (
 
-let k_global_def = (fun lid _63_19 -> (match (_63_19) with
-| (FStar_Syntax_Syntax.Sig_inductive_typ (_63_654, _63_656, _63_658, _63_660, _63_662, datas, _63_665, _63_667), _63_671) -> begin
+let k_global_def = (fun lid _63_22 -> (match (_63_22) with
+| (FStar_Syntax_Syntax.Sig_inductive_typ (_63_703, _63_705, _63_707, _63_709, _63_711, datas, _63_714, _63_716), _63_720) -> begin
 Some (datas)
 end
-| _63_674 -> begin
+| _63_723 -> begin
 None
 end))
-in (resolve_in_open_namespaces' env lid (fun _63_677 -> None) (fun _63_675 -> None) k_global_def)))
+in (resolve_in_open_namespaces' env lid (fun _63_726 -> None) (fun _63_724 -> None) k_global_def)))
 
 
 let record_cache_aux : ((Prims.unit  ->  Prims.unit) * (Prims.unit  ->  Prims.unit) * (Prims.unit  ->  record_or_dc Prims.list) * (record_or_dc  ->  Prims.unit) * (Prims.unit  ->  Prims.unit)) = (
@@ -905,46 +1021,46 @@ let record_cache_aux : ((Prims.unit  ->  Prims.unit) * (Prims.unit  ->  Prims.un
 let record_cache = (FStar_Util.mk_ref (([])::[]))
 in (
 
-let push = (fun _63_681 -> (match (()) with
+let push = (fun _63_730 -> (match (()) with
 | () -> begin
-(let _158_553 = (let _158_552 = (let _158_550 = (FStar_ST.read record_cache)
-in (FStar_List.hd _158_550))
-in (let _158_551 = (FStar_ST.read record_cache)
-in (_158_552)::_158_551))
-in (FStar_ST.op_Colon_Equals record_cache _158_553))
+(let _158_610 = (let _158_609 = (let _158_607 = (FStar_ST.read record_cache)
+in (FStar_List.hd _158_607))
+in (let _158_608 = (FStar_ST.read record_cache)
+in (_158_609)::_158_608))
+in (FStar_ST.op_Colon_Equals record_cache _158_610))
 end))
 in (
 
-let pop = (fun _63_683 -> (match (()) with
+let pop = (fun _63_732 -> (match (()) with
 | () -> begin
-(let _158_557 = (let _158_556 = (FStar_ST.read record_cache)
-in (FStar_List.tl _158_556))
-in (FStar_ST.op_Colon_Equals record_cache _158_557))
+(let _158_614 = (let _158_613 = (FStar_ST.read record_cache)
+in (FStar_List.tl _158_613))
+in (FStar_ST.op_Colon_Equals record_cache _158_614))
 end))
 in (
 
-let peek = (fun _63_685 -> (match (()) with
+let peek = (fun _63_734 -> (match (()) with
 | () -> begin
-(let _158_560 = (FStar_ST.read record_cache)
-in (FStar_List.hd _158_560))
+(let _158_617 = (FStar_ST.read record_cache)
+in (FStar_List.hd _158_617))
 end))
 in (
 
-let insert = (fun r -> (let _158_567 = (let _158_566 = (let _158_563 = (peek ())
-in (r)::_158_563)
-in (let _158_565 = (let _158_564 = (FStar_ST.read record_cache)
-in (FStar_List.tl _158_564))
-in (_158_566)::_158_565))
-in (FStar_ST.op_Colon_Equals record_cache _158_567)))
+let insert = (fun r -> (let _158_624 = (let _158_623 = (let _158_620 = (peek ())
+in (r)::_158_620)
+in (let _158_622 = (let _158_621 = (FStar_ST.read record_cache)
+in (FStar_List.tl _158_621))
+in (_158_623)::_158_622))
+in (FStar_ST.op_Colon_Equals record_cache _158_624)))
 in (
 
-let commit = (fun _63_689 -> (match (()) with
+let commit = (fun _63_738 -> (match (()) with
 | () -> begin
 (match ((FStar_ST.read record_cache)) with
-| (hd)::(_63_692)::tl -> begin
+| (hd)::(_63_741)::tl -> begin
 (FStar_ST.op_Colon_Equals record_cache ((hd)::tl))
 end
-| _63_697 -> begin
+| _63_746 -> begin
 (FStar_All.failwith "Impossible")
 end)
 end))
@@ -953,122 +1069,176 @@ in ((push), (pop), (peek), (insert), (commit))))))))
 
 let push_record_cache : Prims.unit  ->  Prims.unit = (
 
-let _63_707 = record_cache_aux
-in (match (_63_707) with
-| (push, _63_700, _63_702, _63_704, _63_706) -> begin
+let _63_756 = record_cache_aux
+in (match (_63_756) with
+| (push, _63_749, _63_751, _63_753, _63_755) -> begin
 push
 end))
 
 
 let pop_record_cache : Prims.unit  ->  Prims.unit = (
 
-let _63_717 = record_cache_aux
-in (match (_63_717) with
-| (_63_709, pop, _63_712, _63_714, _63_716) -> begin
+let _63_766 = record_cache_aux
+in (match (_63_766) with
+| (_63_758, pop, _63_761, _63_763, _63_765) -> begin
 pop
 end))
 
 
 let peek_record_cache : Prims.unit  ->  record_or_dc Prims.list = (
 
-let _63_727 = record_cache_aux
-in (match (_63_727) with
-| (_63_719, _63_721, peek, _63_724, _63_726) -> begin
+let _63_776 = record_cache_aux
+in (match (_63_776) with
+| (_63_768, _63_770, peek, _63_773, _63_775) -> begin
 peek
 end))
 
 
 let insert_record_cache : record_or_dc  ->  Prims.unit = (
 
-let _63_737 = record_cache_aux
-in (match (_63_737) with
-| (_63_729, _63_731, _63_733, insert, _63_736) -> begin
+let _63_786 = record_cache_aux
+in (match (_63_786) with
+| (_63_778, _63_780, _63_782, insert, _63_785) -> begin
 insert
 end))
 
 
 let commit_record_cache : Prims.unit  ->  Prims.unit = (
 
-let _63_747 = record_cache_aux
-in (match (_63_747) with
-| (_63_739, _63_741, _63_743, _63_745, commit) -> begin
+let _63_796 = record_cache_aux
+in (match (_63_796) with
+| (_63_788, _63_790, _63_792, _63_794, commit) -> begin
 commit
 end))
 
 
-let extract_record : env  ->  scope_mod Prims.list FStar_ST.ref  ->  FStar_Syntax_Syntax.sigelt  ->  Prims.unit = (fun e new_globs _63_23 -> (match (_63_23) with
-| FStar_Syntax_Syntax.Sig_bundle (sigs, _63_753, _63_755, _63_757) -> begin
+let extract_record : env  ->  scope_mod Prims.list FStar_ST.ref  ->  FStar_Syntax_Syntax.sigelt  ->  Prims.unit = (fun e new_globs _63_26 -> (match (_63_26) with
+| FStar_Syntax_Syntax.Sig_bundle (sigs, _63_802, _63_804, _63_806) -> begin
 (
 
-let is_rec = (FStar_Util.for_some (fun _63_20 -> (match (_63_20) with
+let is_rec = (FStar_Util.for_some (fun _63_23 -> (match (_63_23) with
 | (FStar_Syntax_Syntax.RecordType (_)) | (FStar_Syntax_Syntax.RecordConstructor (_)) -> begin
 true
 end
-| _63_768 -> begin
+| _63_817 -> begin
 false
 end)))
 in (
 
-let find_dc = (fun dc -> (FStar_All.pipe_right sigs (FStar_Util.find_opt (fun _63_21 -> (match (_63_21) with
-| FStar_Syntax_Syntax.Sig_datacon (lid, _63_775, _63_777, _63_779, _63_781, _63_783, _63_785, _63_787) -> begin
+let find_dc = (fun dc -> (FStar_All.pipe_right sigs (FStar_Util.find_opt (fun _63_24 -> (match (_63_24) with
+| FStar_Syntax_Syntax.Sig_datacon (lid, _63_824, _63_826, _63_828, _63_830, _63_832, _63_834, _63_836) -> begin
 (FStar_Ident.lid_equals dc lid)
 end
-| _63_791 -> begin
+| _63_840 -> begin
 false
 end)))))
-in (FStar_All.pipe_right sigs (FStar_List.iter (fun _63_22 -> (match (_63_22) with
-| FStar_Syntax_Syntax.Sig_inductive_typ (typename, univs, parms, _63_797, _63_799, (dc)::[], tags, _63_804) -> begin
-(match ((let _158_672 = (find_dc dc)
-in (FStar_All.pipe_left FStar_Util.must _158_672))) with
-| FStar_Syntax_Syntax.Sig_datacon (constrname, _63_809, t, _63_812, _63_814, _63_816, _63_818, _63_820) -> begin
+in (FStar_All.pipe_right sigs (FStar_List.iter (fun _63_25 -> (match (_63_25) with
+| FStar_Syntax_Syntax.Sig_inductive_typ (typename, univs, parms, _63_846, _63_848, (dc)::[], tags, _63_853) -> begin
+(match ((let _158_729 = (find_dc dc)
+in (FStar_All.pipe_left FStar_Util.must _158_729))) with
+| FStar_Syntax_Syntax.Sig_datacon (constrname, _63_858, t, _63_861, _63_863, _63_865, _63_867, _63_869) -> begin
 (
 
-let _63_826 = (FStar_Syntax_Util.arrow_formals t)
-in (match (_63_826) with
-| (formals, _63_825) -> begin
+let _63_875 = (FStar_Syntax_Util.arrow_formals t)
+in (match (_63_875) with
+| (formals, _63_874) -> begin
 (
 
 let is_rec = (is_rec tags)
 in (
 
-let fields = (FStar_All.pipe_right formals (FStar_List.collect (fun _63_830 -> (match (_63_830) with
+let formals' = (FStar_All.pipe_right formals (FStar_List.collect (fun _63_879 -> (match (_63_879) with
 | (x, q) -> begin
 if ((FStar_Syntax_Syntax.is_null_bv x) || (is_rec && (FStar_Syntax_Syntax.is_implicit q))) then begin
 []
 end else begin
-(let _158_676 = (let _158_675 = (let _158_674 = if is_rec then begin
+(((x), (q)))::[]
+end
+end))))
+in (
+
+let fields' = (FStar_All.pipe_right formals' (FStar_List.map (fun _63_883 -> (match (_63_883) with
+| (x, q) -> begin
+(let _158_732 = if is_rec then begin
 (FStar_Syntax_Util.unmangle_field_name x.FStar_Syntax_Syntax.ppname)
 end else begin
 x.FStar_Syntax_Syntax.ppname
 end
-in (FStar_Syntax_Util.mk_field_projector_name_from_ident constrname _158_674))
-in ((_158_675), (x.FStar_Syntax_Syntax.sort)))
-in (_158_676)::[])
-end
+in ((_158_732), (x.FStar_Syntax_Syntax.sort)))
+end))))
+in (
+
+let fields = (FStar_All.pipe_right fields' (FStar_List.map (fun _63_887 -> (match (_63_887) with
+| (xid, xsort) -> begin
+(let _158_734 = (FStar_Syntax_Util.mk_field_projector_name_from_ident constrname xid)
+in ((_158_734), (xsort)))
 end))))
 in (
 
 let record = {typename = typename; constrname = constrname; parms = parms; fields = fields; is_record = is_rec}
 in (
 
-let _63_833 = (let _158_678 = (let _158_677 = (FStar_ST.read new_globs)
-in (Record_or_dc (record))::_158_677)
-in (FStar_ST.op_Colon_Equals new_globs _158_678))
+let _63_890 = (let _158_736 = (let _158_735 = (FStar_ST.read new_globs)
+in (Record_or_dc (record))::_158_735)
+in (FStar_ST.op_Colon_Equals new_globs _158_736))
+in (match (()) with
+| () -> begin
+(
+
+let _63_904 = (
+
+let add_field = (fun _63_895 -> (match (_63_895) with
+| (id, _63_894) -> begin
+(
+
+let modul = (let _158_739 = (FStar_Ident.lid_of_ids constrname.FStar_Ident.ns)
+in _158_739.FStar_Ident.str)
+in (match ((get_exported_id_set e modul)) with
+| Some (my_ex) -> begin
+(
+
+let my_exported_ids = (my_ex Exported_id_field)
+in (
+
+let _63_900 = (let _158_742 = (let _158_741 = (FStar_ST.read my_exported_ids)
+in (FStar_Util.set_add id.FStar_Ident.idText _158_741))
+in (FStar_ST.op_Colon_Equals my_exported_ids _158_742))
+in (match (()) with
+| () -> begin
+(
+
+let projname = (let _158_744 = (let _158_743 = (FStar_Syntax_Util.mk_field_projector_name_from_ident constrname id)
+in _158_743.FStar_Ident.ident)
+in _158_744.FStar_Ident.idText)
+in (
+
+let _63_902 = (let _158_746 = (let _158_745 = (FStar_ST.read my_exported_ids)
+in (FStar_Util.set_add projname _158_745))
+in (FStar_ST.op_Colon_Equals my_exported_ids _158_746))
+in ()))
+end)))
+end
+| None -> begin
+()
+end))
+end))
+in (FStar_List.iter add_field fields'))
 in (match (()) with
 | () -> begin
 (insert_record_cache record)
-end)))))
+end))
+end)))))))
 end))
 end
-| _63_835 -> begin
+| _63_906 -> begin
 ()
 end)
 end
-| _63_837 -> begin
+| _63_908 -> begin
 ()
 end))))))
 end
-| _63_839 -> begin
+| _63_910 -> begin
 ()
 end))
 
@@ -1080,22 +1250,22 @@ in (
 
 let find_in_cache = (fun fieldname -> (
 
-let _63_847 = ((fieldname.FStar_Ident.ns), (fieldname.FStar_Ident.ident))
-in (match (_63_847) with
+let _63_918 = ((fieldname.FStar_Ident.ns), (fieldname.FStar_Ident.ident))
+in (match (_63_918) with
 | (ns, id) -> begin
-(let _158_689 = (peek_record_cache ())
-in (FStar_Util.find_map _158_689 (fun record -> (let _158_688 = (find_in_record ns id record (fun r -> Cont_ok (r)))
-in (option_of_cont (fun _63_850 -> None) _158_688)))))
+(let _158_757 = (peek_record_cache ())
+in (FStar_Util.find_map _158_757 (fun record -> (let _158_756 = (find_in_record ns id record (fun r -> Cont_ok (r)))
+in (option_of_cont (fun _63_921 -> None) _158_756)))))
 end)))
-in (resolve_in_open_namespaces'' env fieldname (fun _63_860 -> Cont_ignore) (fun _63_858 -> Cont_ignore) (fun r -> Cont_ok (r)) (fun k fn -> (let _158_695 = (find_in_cache fn)
-in (cont_of_option k _158_695))) (fun k _63_853 -> k)))))
+in (resolve_in_open_namespaces'' env fieldname Exported_id_field (fun _63_930 -> Cont_ignore) (fun _63_928 -> Cont_ignore) (fun r -> Cont_ok (r)) (fun fn -> (let _158_762 = (find_in_cache fn)
+in (cont_of_option Cont_ignore _158_762))) (fun k _63_924 -> k)))))
 
 
 let try_lookup_record_by_field_name : env  ->  FStar_Ident.lident  ->  (record_or_dc * FStar_Ident.lident) Prims.option = (fun env fieldname -> (match ((try_lookup_record_or_dc_by_field_name env fieldname)) with
 | Some (r, f) when r.is_record -> begin
 Some (((r), (f)))
 end
-| _63_869 -> begin
+| _63_939 -> begin
 None
 end))
 
@@ -1104,7 +1274,7 @@ let try_lookup_projector_by_field_name : env  ->  FStar_Ident.lident  ->  (FStar
 | Some (r, f) -> begin
 Some (((f), (r.is_record)))
 end
-| _63_877 -> begin
+| _63_947 -> begin
 None
 end))
 
@@ -1113,18 +1283,18 @@ let qualify_field_to_record : env  ->  record_or_dc  ->  FStar_Ident.lident  ->
 
 let qualify = (fun fieldname -> (
 
-let _63_885 = ((fieldname.FStar_Ident.ns), (fieldname.FStar_Ident.ident))
-in (match (_63_885) with
+let _63_955 = ((fieldname.FStar_Ident.ns), (fieldname.FStar_Ident.ident))
+in (match (_63_955) with
 | (ns, fieldname) -> begin
 (
 
 let constrname = recd.constrname.FStar_Ident.ident
 in (
 
-let fname = (let _158_714 = (FStar_Ident.lid_of_ids (FStar_List.append ns ((constrname)::[])))
-in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_714 fieldname))
-in (FStar_Util.find_map recd.fields (fun _63_891 -> (match (_63_891) with
-| (f, _63_890) -> begin
+let fname = (let _158_781 = (FStar_Ident.lid_of_ids (FStar_List.append ns ((constrname)::[])))
+in (FStar_Syntax_Util.mk_field_projector_name_from_ident _158_781 fieldname))
+in (FStar_Util.find_map recd.fields (fun _63_961 -> (match (_63_961) with
+| (f, _63_960) -> begin
 if (FStar_Ident.lid_equals fname f) then begin
 Some (fname)
 end else begin
@@ -1132,29 +1302,70 @@ None
 end
 end)))))
 end)))
-in (resolve_in_open_namespaces'' env f (fun _63_900 -> Cont_ignore) (fun _63_898 -> Cont_ignore) (fun r -> Cont_ok ((Prims.snd r))) (fun k fn -> (let _158_721 = (qualify fn)
-in (cont_of_option k _158_721))) (fun k _63_893 -> k))))
+in (resolve_in_open_namespaces'' env f Exported_id_field (fun _63_969 -> Cont_ignore) (fun _63_967 -> Cont_ignore) (fun r -> Cont_ok ((Prims.snd r))) (fun fn -> (let _158_787 = (qualify fn)
+in (cont_of_option Cont_ignore _158_787))) (fun k _63_963 -> k))))
+
+
+let string_set_ref_new : Prims.unit  ->  Prims.string FStar_Util.set FStar_ST.ref = (fun _63_971 -> (match (()) with
+| () -> begin
+(let _158_792 = (FStar_Util.new_set FStar_Util.compare FStar_Util.hashcode)
+in (FStar_Util.mk_ref _158_792))
+end))
+
+
+let exported_id_set_new : Prims.unit  ->  exported_id_kind  ->  Prims.string FStar_Util.set FStar_ST.ref = (fun _63_972 -> (match (()) with
+| () -> begin
+(
+
+let term_type_set = (string_set_ref_new ())
+in (
+
+let field_set = (string_set_ref_new ())
+in (fun _63_27 -> (match (_63_27) with
+| Exported_id_term_type -> begin
+term_type_set
+end
+| Exported_id_field -> begin
+field_set
+end))))
+end))
+
+
+let empty_include_smap : FStar_Ident.lident Prims.list FStar_ST.ref FStar_Util.smap = (new_sigmap ())
+
+
+let empty_exported_id_smap : exported_id_set FStar_Util.smap = (new_sigmap ())
 
 
 let unique : Prims.bool  ->  Prims.bool  ->  env  ->  FStar_Ident.lident  ->  Prims.bool = (fun any_val exclude_if env lid -> (
 
+let filter_scope_mods = (fun _63_28 -> (match (_63_28) with
+| Rec_binding (_63_984) -> begin
+true
+end
+| _63_987 -> begin
+false
+end))
+in (
+
 let this_env = (
 
-let _63_906 = env
-in {curmodule = _63_906.curmodule; curmonad = _63_906.curmonad; modules = _63_906.modules; scope_mods = []; sigaccum = _63_906.sigaccum; sigmap = _63_906.sigmap; default_result_effect = _63_906.default_result_effect; iface = _63_906.iface; admitted_iface = _63_906.admitted_iface; expect_typ = _63_906.expect_typ})
-in (match ((try_lookup_lid' any_val exclude_if env lid)) with
+let _63_989 = env
+in (let _158_812 = (FStar_List.filter filter_scope_mods env.scope_mods)
+in {curmodule = _63_989.curmodule; curmonad = _63_989.curmonad; modules = _63_989.modules; scope_mods = _158_812; exported_ids = empty_exported_id_smap; trans_exported_ids = _63_989.trans_exported_ids; includes = empty_include_smap; sigaccum = _63_989.sigaccum; sigmap = _63_989.sigmap; default_result_effect = _63_989.default_result_effect; iface = _63_989.iface; admitted_iface = _63_989.admitted_iface; expect_typ = _63_989.expect_typ}))
+in (match ((try_lookup_lid' any_val exclude_if this_env lid)) with
 | None -> begin
 true
 end
-| Some (_63_911) -> begin
+| Some (_63_994) -> begin
 false
-end)))
+end))))
 
 
 let push_scope_mod : env  ->  scope_mod  ->  env = (fun env scope_mod -> (
 
-let _63_915 = env
-in {curmodule = _63_915.curmodule; curmonad = _63_915.curmonad; modules = _63_915.modules; scope_mods = (scope_mod)::env.scope_mods; sigaccum = _63_915.sigaccum; sigmap = _63_915.sigmap; default_result_effect = _63_915.default_result_effect; iface = _63_915.iface; admitted_iface = _63_915.admitted_iface; expect_typ = _63_915.expect_typ}))
+let _63_998 = env
+in {curmodule = _63_998.curmodule; curmonad = _63_998.curmonad; modules = _63_998.modules; scope_mods = (scope_mod)::env.scope_mods; exported_ids = _63_998.exported_ids; trans_exported_ids = _63_998.trans_exported_ids; includes = _63_998.includes; sigaccum = _63_998.sigaccum; sigmap = _63_998.sigmap; default_result_effect = _63_998.default_result_effect; iface = _63_998.iface; admitted_iface = _63_998.admitted_iface; expect_typ = _63_998.expect_typ}))
 
 
 let push_bv' : env  ->  FStar_Ident.ident  ->  Prims.bool  ->  (env * FStar_Syntax_Syntax.bv) = (fun env x is_mutable -> (
@@ -1187,9 +1398,9 @@ let sopt = (FStar_Util.smap_try_find (sigmap env) l.FStar_Ident.str)
 in (
 
 let r = (match (sopt) with
-| Some (se, _63_936) -> begin
-(match ((let _158_762 = (FStar_Syntax_Util.lids_of_sigelt se)
-in (FStar_Util.find_opt (FStar_Ident.lid_equals l) _158_762))) with
+| Some (se, _63_1019) -> begin
+(match ((let _158_843 = (FStar_Syntax_Util.lids_of_sigelt se)
+in (FStar_Util.find_opt (FStar_Ident.lid_equals l) _158_843))) with
 | Some (l) -> begin
 (FStar_All.pipe_left FStar_Range.string_of_range (FStar_Ident.range_of_lid l))
 end
@@ -1200,10 +1411,10 @@ end
 | None -> begin
 "<unknown>"
 end)
-in (let _158_765 = (let _158_764 = (let _158_763 = (FStar_Util.format2 "Duplicate top-level names [%s]; previously declared at %s" (FStar_Ident.text_of_lid l) r)
-in ((_158_763), ((FStar_Ident.range_of_lid l))))
-in FStar_Syntax_Syntax.Error (_158_764))
-in (Prims.raise _158_765)))))
+in (let _158_846 = (let _158_845 = (let _158_844 = (FStar_Util.format2 "Duplicate top-level names [%s]; previously declared at %s" (FStar_Ident.text_of_lid l) r)
+in ((_158_844), ((FStar_Ident.range_of_lid l))))
+in FStar_Syntax_Syntax.Error (_158_845))
+in (Prims.raise _158_846)))))
 in (
 
 let globals = (FStar_ST.alloc env.scope_mods)
@@ -1211,17 +1422,17 @@ in (
 
 let env = (
 
-let _63_955 = (match (s) with
-| FStar_Syntax_Syntax.Sig_let (_63_946) -> begin
+let _63_1038 = (match (s) with
+| FStar_Syntax_Syntax.Sig_let (_63_1029) -> begin
 ((false), (true))
 end
-| FStar_Syntax_Syntax.Sig_bundle (_63_949) -> begin
+| FStar_Syntax_Syntax.Sig_bundle (_63_1032) -> begin
 ((true), (true))
 end
-| _63_952 -> begin
+| _63_1035 -> begin
 ((false), (false))
 end)
-in (match (_63_955) with
+in (match (_63_1038) with
 | (any_val, exclude_if) -> begin
 (
 
@@ -1234,11 +1445,11 @@ end))) with
 | None -> begin
 (
 
-let _63_959 = (extract_record env globals s)
+let _63_1042 = (extract_record env globals s)
 in (
 
-let _63_961 = env
-in {curmodule = _63_961.curmodule; curmonad = _63_961.curmonad; modules = _63_961.modules; scope_mods = _63_961.scope_mods; sigaccum = (s)::env.sigaccum; sigmap = _63_961.sigmap; default_result_effect = _63_961.default_result_effect; iface = _63_961.iface; admitted_iface = _63_961.admitted_iface; expect_typ = _63_961.expect_typ}))
+let _63_1044 = env
+in {curmodule = _63_1044.curmodule; curmonad = _63_1044.curmonad; modules = _63_1044.modules; scope_mods = _63_1044.scope_mods; exported_ids = _63_1044.exported_ids; trans_exported_ids = _63_1044.trans_exported_ids; includes = _63_1044.includes; sigaccum = (s)::env.sigaccum; sigmap = _63_1044.sigmap; default_result_effect = _63_1044.default_result_effect; iface = _63_1044.iface; admitted_iface = _63_1044.admitted_iface; expect_typ = _63_1044.expect_typ}))
 end
 | Some (l) -> begin
 (err l)
@@ -1248,85 +1459,188 @@ in (
 
 let env = (
 
-let _63_966 = env
-in (let _158_767 = (FStar_ST.read globals)
-in {curmodule = _63_966.curmodule; curmonad = _63_966.curmonad; modules = _63_966.modules; scope_mods = _158_767; sigaccum = _63_966.sigaccum; sigmap = _63_966.sigmap; default_result_effect = _63_966.default_result_effect; iface = _63_966.iface; admitted_iface = _63_966.admitted_iface; expect_typ = _63_966.expect_typ}))
+let _63_1049 = env
+in (let _158_848 = (FStar_ST.read globals)
+in {curmodule = _63_1049.curmodule; curmonad = _63_1049.curmonad; modules = _63_1049.modules; scope_mods = _158_848; exported_ids = _63_1049.exported_ids; trans_exported_ids = _63_1049.trans_exported_ids; includes = _63_1049.includes; sigaccum = _63_1049.sigaccum; sigmap = _63_1049.sigmap; default_result_effect = _63_1049.default_result_effect; iface = _63_1049.iface; admitted_iface = _63_1049.admitted_iface; expect_typ = _63_1049.expect_typ}))
 in (
 
-let _63_983 = (match (s) with
-| FStar_Syntax_Syntax.Sig_bundle (ses, _63_971, _63_973, _63_975) -> begin
-(let _158_770 = (FStar_List.map (fun se -> (let _158_769 = (FStar_Syntax_Util.lids_of_sigelt se)
-in ((_158_769), (se)))) ses)
-in ((env), (_158_770)))
-end
-| _63_980 -> begin
-(let _158_773 = (let _158_772 = (let _158_771 = (FStar_Syntax_Util.lids_of_sigelt s)
-in ((_158_771), (s)))
-in (_158_772)::[])
-in ((env), (_158_773)))
+let _63_1066 = (match (s) with
+| FStar_Syntax_Syntax.Sig_bundle (ses, _63_1054, _63_1056, _63_1058) -> begin
+(let _158_851 = (FStar_List.map (fun se -> (let _158_850 = (FStar_Syntax_Util.lids_of_sigelt se)
+in ((_158_850), (se)))) ses)
+in ((env), (_158_851)))
+end
+| _63_1063 -> begin
+(let _158_854 = (let _158_853 = (let _158_852 = (FStar_Syntax_Util.lids_of_sigelt s)
+in ((_158_852), (s)))
+in (_158_853)::[])
+in ((env), (_158_854)))
 end)
-in (match (_63_983) with
+in (match (_63_1066) with
 | (env, lss) -> begin
 (
 
-let _63_989 = (FStar_All.pipe_right lss (FStar_List.iter (fun _63_986 -> (match (_63_986) with
+let _63_1078 = (FStar_All.pipe_right lss (FStar_List.iter (fun _63_1069 -> (match (_63_1069) with
 | (lids, se) -> begin
 (FStar_All.pipe_right lids (FStar_List.iter (fun lid -> (
 
-let _63_988 = (let _158_777 = (let _158_776 = (FStar_ST.read globals)
-in (Top_level_def (lid.FStar_Ident.ident))::_158_776)
-in (FStar_ST.op_Colon_Equals globals _158_777))
+let _63_1071 = (let _158_858 = (let _158_857 = (FStar_ST.read globals)
+in (Top_level_def (lid.FStar_Ident.ident))::_158_857)
+in (FStar_ST.op_Colon_Equals globals _158_858))
+in (match (()) with
+| () -> begin
+(
+
+let modul = (let _158_859 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
+in _158_859.FStar_Ident.str)
+in (
+
+let _63_1077 = (match ((get_exported_id_set env modul)) with
+| Some (f) -> begin
+(
+
+let my_exported_ids = (f Exported_id_term_type)
+in (let _158_862 = (let _158_861 = (FStar_ST.read my_exported_ids)
+in (FStar_Util.set_add lid.FStar_Ident.ident.FStar_Ident.idText _158_861))
+in (FStar_ST.op_Colon_Equals my_exported_ids _158_862)))
+end
+| None -> begin
+()
+end)
 in (match (()) with
 | () -> begin
 (FStar_Util.smap_add (sigmap env) lid.FStar_Ident.str ((se), ((env.iface && (not (env.admitted_iface))))))
+end)))
 end)))))
 end))))
 in (
 
 let env = (
 
-let _63_991 = env
-in (let _158_778 = (FStar_ST.read globals)
-in {curmodule = _63_991.curmodule; curmonad = _63_991.curmonad; modules = _63_991.modules; scope_mods = _158_778; sigaccum = _63_991.sigaccum; sigmap = _63_991.sigmap; default_result_effect = _63_991.default_result_effect; iface = _63_991.iface; admitted_iface = _63_991.admitted_iface; expect_typ = _63_991.expect_typ}))
+let _63_1080 = env
+in (let _158_863 = (FStar_ST.read globals)
+in {curmodule = _63_1080.curmodule; curmonad = _63_1080.curmonad; modules = _63_1080.modules; scope_mods = _158_863; exported_ids = _63_1080.exported_ids; trans_exported_ids = _63_1080.trans_exported_ids; includes = _63_1080.includes; sigaccum = _63_1080.sigaccum; sigmap = _63_1080.sigmap; default_result_effect = _63_1080.default_result_effect; iface = _63_1080.iface; admitted_iface = _63_1080.admitted_iface; expect_typ = _63_1080.expect_typ}))
 in env))
 end)))))))
 
 
 let push_namespace : env  ->  FStar_Ident.lident  ->  env = (fun env ns -> (
 
-let _63_1006 = (match ((resolve_module_name env ns false)) with
+let _63_1095 = (match ((resolve_module_name env ns false)) with
 | None -> begin
 (
 
 let modules = env.modules
-in if (FStar_All.pipe_right modules (FStar_Util.for_some (fun _63_1001 -> (match (_63_1001) with
-| (m, _63_1000) -> begin
+in if (FStar_All.pipe_right modules (FStar_Util.for_some (fun _63_1090 -> (match (_63_1090) with
+| (m, _63_1089) -> begin
 (FStar_Util.starts_with (Prims.strcat (FStar_Ident.text_of_lid m) ".") (Prims.strcat (FStar_Ident.text_of_lid ns) "."))
 end)))) then begin
 ((ns), (Open_namespace))
 end else begin
-(let _158_786 = (let _158_785 = (let _158_784 = (FStar_Util.format1 "Namespace %s cannot be found" (FStar_Ident.text_of_lid ns))
-in ((_158_784), ((FStar_Ident.range_of_lid ns))))
-in FStar_Syntax_Syntax.Error (_158_785))
-in (Prims.raise _158_786))
+(let _158_871 = (let _158_870 = (let _158_869 = (FStar_Util.format1 "Namespace %s cannot be found" (FStar_Ident.text_of_lid ns))
+in ((_158_869), ((FStar_Ident.range_of_lid ns))))
+in FStar_Syntax_Syntax.Error (_158_870))
+in (Prims.raise _158_871))
 end)
 end
 | Some (ns') -> begin
 ((ns'), (Open_module))
 end)
-in (match (_63_1006) with
+in (match (_63_1095) with
 | (ns', kd) -> begin
 (push_scope_mod env (Open_module_or_namespace (((ns'), (kd)))))
 end)))
 
 
+let push_include : env  ->  FStar_Ident.lident  ->  env = (fun env ns -> (match ((resolve_module_name env ns false)) with
+| Some (ns) -> begin
+(
+
+let env = (push_scope_mod env (Open_module_or_namespace (((ns), (Open_module)))))
+in (
+
+let curmod = (let _158_876 = (current_module env)
+in _158_876.FStar_Ident.str)
+in (
+
+let _63_1105 = (match ((FStar_Util.smap_try_find env.includes curmod)) with
+| None -> begin
+()
+end
+| Some (incl) -> begin
+(let _158_878 = (let _158_877 = (FStar_ST.read incl)
+in (ns)::_158_877)
+in (FStar_ST.op_Colon_Equals incl _158_878))
+end)
+in (match (()) with
+| () -> begin
+(match ((get_trans_exported_id_set env ns.FStar_Ident.str)) with
+| Some (ns_trans_exports) -> begin
+(
+
+let _63_1122 = (match ((let _158_885 = (get_exported_id_set env curmod)
+in (let _158_884 = (get_trans_exported_id_set env curmod)
+in ((_158_885), (_158_884))))) with
+| (Some (cur_exports), Some (cur_trans_exports)) -> begin
+(
+
+let update_exports = (fun k -> (
+
+let ns_ex = (let _158_890 = (ns_trans_exports k)
+in (FStar_ST.read _158_890))
+in (
+
+let ex = (cur_exports k)
+in (
+
+let _63_1117 = (let _158_892 = (let _158_891 = (FStar_ST.read ex)
+in (FStar_Util.set_difference _158_891 ns_ex))
+in (FStar_ST.op_Colon_Equals ex _158_892))
+in (match (()) with
+| () -> begin
+(
+
+let trans_ex = (cur_trans_exports k)
+in (
+
+let _63_1119 = (let _158_894 = (let _158_893 = (FStar_ST.read ex)
+in (FStar_Util.set_union _158_893 ns_ex))
+in (FStar_ST.op_Colon_Equals trans_ex _158_894))
+in ()))
+end)))))
+in (FStar_List.iter update_exports all_exported_id_kinds))
+end
+| _63_1121 -> begin
+()
+end)
+in (match (()) with
+| () -> begin
+env
+end))
+end
+| None -> begin
+(let _158_903 = (let _158_902 = (let _158_901 = (FStar_Util.format1 "include: Module %s was not prepared" ns.FStar_Ident.str)
+in ((_158_901), ((FStar_Ident.range_of_lid ns))))
+in FStar_Syntax_Syntax.Error (_158_902))
+in (Prims.raise _158_903))
+end)
+end))))
+end
+| _63_1125 -> begin
+(let _158_906 = (let _158_905 = (let _158_904 = (FStar_Util.format1 "include: Module %s cannot be found" ns.FStar_Ident.str)
+in ((_158_904), ((FStar_Ident.range_of_lid ns))))
+in FStar_Syntax_Syntax.Error (_158_905))
+in (Prims.raise _158_906))
+end))
+
+
 let push_module_abbrev : env  ->  FStar_Ident.ident  ->  FStar_Ident.lident  ->  env = (fun env x l -> if (module_is_defined env l) then begin
 (push_scope_mod env (Module_abbrev (((x), (l)))))
 end else begin
-(let _158_795 = (let _158_794 = (let _158_793 = (FStar_Util.format1 "Module %s cannot be found" (FStar_Ident.text_of_lid l))
-in ((_158_793), ((FStar_Ident.range_of_lid l))))
-in FStar_Syntax_Syntax.Error (_158_794))
-in (Prims.raise _158_795))
+(let _158_915 = (let _158_914 = (let _158_913 = (FStar_Util.format1 "Module %s cannot be found" (FStar_Ident.text_of_lid l))
+in ((_158_913), ((FStar_Ident.range_of_lid l))))
+in FStar_Syntax_Syntax.Error (_158_914))
+in (Prims.raise _158_915))
 end)
 
 
@@ -1336,62 +1650,62 @@ let check_admits : env  ->  Prims.unit = (fun env -> (FStar_All.pipe_right env.s
 | None -> begin
 (
 
-let _63_1020 = (let _158_801 = (let _158_800 = (FStar_Range.string_of_range (FStar_Ident.range_of_lid l))
-in (let _158_799 = (FStar_Syntax_Print.lid_to_string l)
-in (FStar_Util.format2 "%s: Warning: Admitting %s without a definition\n" _158_800 _158_799)))
-in (FStar_Util.print_string _158_801))
+let _63_1139 = (let _158_921 = (let _158_920 = (FStar_Range.string_of_range (FStar_Ident.range_of_lid l))
+in (let _158_919 = (FStar_Syntax_Print.lid_to_string l)
+in (FStar_Util.format2 "%s: Warning: Admitting %s without a definition\n" _158_920 _158_919)))
+in (FStar_Util.print_string _158_921))
 in (FStar_Util.smap_add (sigmap env) l.FStar_Ident.str ((FStar_Syntax_Syntax.Sig_declare_typ (((l), (u), (t), ((FStar_Syntax_Syntax.Assumption)::quals), (r)))), (false))))
 end
-| Some (_63_1023) -> begin
+| Some (_63_1142) -> begin
 ()
 end)
 end
-| _63_1026 -> begin
+| _63_1145 -> begin
 ()
 end)))))
 
 
 let finish : env  ->  FStar_Syntax_Syntax.modul  ->  env = (fun env modul -> (
 
-let _63_1086 = (FStar_All.pipe_right modul.FStar_Syntax_Syntax.declarations (FStar_List.iter (fun _63_25 -> (match (_63_25) with
-| FStar_Syntax_Syntax.Sig_bundle (ses, quals, _63_1033, _63_1035) -> begin
+let _63_1205 = (FStar_All.pipe_right modul.FStar_Syntax_Syntax.declarations (FStar_List.iter (fun _63_30 -> (match (_63_30) with
+| FStar_Syntax_Syntax.Sig_bundle (ses, quals, _63_1152, _63_1154) -> begin
 if ((FStar_List.contains FStar_Syntax_Syntax.Private quals) || (FStar_List.contains FStar_Syntax_Syntax.Abstract quals)) then begin
-(FStar_All.pipe_right ses (FStar_List.iter (fun _63_24 -> (match (_63_24) with
-| FStar_Syntax_Syntax.Sig_datacon (lid, _63_1041, _63_1043, _63_1045, _63_1047, _63_1049, _63_1051, _63_1053) -> begin
+(FStar_All.pipe_right ses (FStar_List.iter (fun _63_29 -> (match (_63_29) with
+| FStar_Syntax_Syntax.Sig_datacon (lid, _63_1160, _63_1162, _63_1164, _63_1166, _63_1168, _63_1170, _63_1172) -> begin
 (FStar_Util.smap_remove (sigmap env) lid.FStar_Ident.str)
 end
-| _63_1057 -> begin
+| _63_1176 -> begin
 ()
 end))))
 end else begin
 ()
 end
 end
-| FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_1060, _63_1062, quals, _63_1065) -> begin
+| FStar_Syntax_Syntax.Sig_declare_typ (lid, _63_1179, _63_1181, quals, _63_1184) -> begin
 if (FStar_List.contains FStar_Syntax_Syntax.Private quals) then begin
 (FStar_Util.smap_remove (sigmap env) lid.FStar_Ident.str)
 end else begin
 ()
 end
 end
-| FStar_Syntax_Syntax.Sig_let ((_63_1069, lbs), r, _63_1074, quals) -> begin
+| FStar_Syntax_Syntax.Sig_let ((_63_1188, lbs), r, _63_1193, quals) -> begin
 (
 
-let _63_1079 = if ((FStar_List.contains FStar_Syntax_Syntax.Private quals) || (FStar_List.contains FStar_Syntax_Syntax.Abstract quals)) then begin
-(FStar_All.pipe_right lbs (FStar_List.iter (fun lb -> (let _158_812 = (let _158_811 = (let _158_810 = (let _158_809 = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
-in _158_809.FStar_Syntax_Syntax.fv_name)
-in _158_810.FStar_Syntax_Syntax.v)
-in _158_811.FStar_Ident.str)
-in (FStar_Util.smap_remove (sigmap env) _158_812)))))
+let _63_1198 = if ((FStar_List.contains FStar_Syntax_Syntax.Private quals) || (FStar_List.contains FStar_Syntax_Syntax.Abstract quals)) then begin
+(FStar_All.pipe_right lbs (FStar_List.iter (fun lb -> (let _158_932 = (let _158_931 = (let _158_930 = (let _158_929 = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
+in _158_929.FStar_Syntax_Syntax.fv_name)
+in _158_930.FStar_Syntax_Syntax.v)
+in _158_931.FStar_Ident.str)
+in (FStar_Util.smap_remove (sigmap env) _158_932)))))
 end else begin
 ()
 end
 in if ((FStar_List.contains FStar_Syntax_Syntax.Abstract quals) && (not ((FStar_List.contains FStar_Syntax_Syntax.Private quals)))) then begin
 (FStar_All.pipe_right lbs (FStar_List.iter (fun lb -> (
 
-let lid = (let _158_815 = (let _158_814 = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
-in _158_814.FStar_Syntax_Syntax.fv_name)
-in _158_815.FStar_Syntax_Syntax.v)
+let lid = (let _158_935 = (let _158_934 = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
+in _158_934.FStar_Syntax_Syntax.fv_name)
+in _158_935.FStar_Syntax_Syntax.v)
 in (
 
 let decl = FStar_Syntax_Syntax.Sig_declare_typ (((lid), (lb.FStar_Syntax_Syntax.lbunivs), (lb.FStar_Syntax_Syntax.lbtyp), ((FStar_Syntax_Syntax.Assumption)::quals), (r)))
@@ -1400,13 +1714,43 @@ end else begin
 ()
 end)
 end
-| _63_1085 -> begin
+| _63_1204 -> begin
 ()
 end))))
 in (
 
-let _63_1088 = env
-in {curmodule = None; curmonad = _63_1088.curmonad; modules = (((modul.FStar_Syntax_Syntax.name), (modul)))::env.modules; scope_mods = []; sigaccum = []; sigmap = _63_1088.sigmap; default_result_effect = _63_1088.default_result_effect; iface = _63_1088.iface; admitted_iface = _63_1088.admitted_iface; expect_typ = _63_1088.expect_typ})))
+let curmod = (let _158_936 = (current_module env)
+in _158_936.FStar_Ident.str)
+in (
+
+let _63_1219 = (match ((let _158_942 = (get_exported_id_set env curmod)
+in (let _158_941 = (get_trans_exported_id_set env curmod)
+in ((_158_942), (_158_941))))) with
+| (Some (cur_ex), Some (cur_trans_ex)) -> begin
+(
+
+let update_exports = (fun eikind -> (
+
+let cur_ex_set = (let _158_947 = (cur_ex eikind)
+in (FStar_ST.read _158_947))
+in (
+
+let cur_trans_ex_set_ref = (cur_trans_ex eikind)
+in (let _158_949 = (let _158_948 = (FStar_ST.read cur_trans_ex_set_ref)
+in (FStar_Util.set_union cur_ex_set _158_948))
+in (FStar_ST.op_Colon_Equals cur_trans_ex_set_ref _158_949)))))
+in (FStar_List.iter update_exports all_exported_id_kinds))
+end
+| _63_1218 -> begin
+()
+end)
+in (match (()) with
+| () -> begin
+(
+
+let _63_1220 = env
+in {curmodule = None; curmonad = _63_1220.curmonad; modules = (((modul.FStar_Syntax_Syntax.name), (modul)))::env.modules; scope_mods = []; exported_ids = _63_1220.exported_ids; trans_exported_ids = _63_1220.trans_exported_ids; includes = _63_1220.includes; sigaccum = []; sigmap = _63_1220.sigmap; default_result_effect = _63_1220.default_result_effect; iface = _63_1220.iface; admitted_iface = _63_1220.admitted_iface; expect_typ = _63_1220.expect_typ})
+end)))))
 
 
 type env_stack_ops =
@@ -1423,45 +1767,45 @@ in (
 
 let push = (fun env -> (
 
-let _63_1099 = (push_record_cache ())
+let _63_1231 = (push_record_cache ())
 in (
 
-let _63_1101 = (let _158_865 = (let _158_864 = (FStar_ST.read stack)
-in (env)::_158_864)
-in (FStar_ST.op_Colon_Equals stack _158_865))
+let _63_1233 = (let _158_1005 = (let _158_1004 = (FStar_ST.read stack)
+in (env)::_158_1004)
+in (FStar_ST.op_Colon_Equals stack _158_1005))
 in (
 
-let _63_1103 = env
-in (let _158_866 = (FStar_Util.smap_copy (sigmap env))
-in {curmodule = _63_1103.curmodule; curmonad = _63_1103.curmonad; modules = _63_1103.modules; scope_mods = _63_1103.scope_mods; sigaccum = _63_1103.sigaccum; sigmap = _158_866; default_result_effect = _63_1103.default_result_effect; iface = _63_1103.iface; admitted_iface = _63_1103.admitted_iface; expect_typ = _63_1103.expect_typ})))))
+let _63_1235 = env
+in (let _158_1006 = (FStar_Util.smap_copy (sigmap env))
+in {curmodule = _63_1235.curmodule; curmonad = _63_1235.curmonad; modules = _63_1235.modules; scope_mods = _63_1235.scope_mods; exported_ids = _63_1235.exported_ids; trans_exported_ids = _63_1235.trans_exported_ids; includes = _63_1235.includes; sigaccum = _63_1235.sigaccum; sigmap = _158_1006; default_result_effect = _63_1235.default_result_effect; iface = _63_1235.iface; admitted_iface = _63_1235.admitted_iface; expect_typ = _63_1235.expect_typ})))))
 in (
 
 let pop = (fun env -> (match ((FStar_ST.read stack)) with
 | (env)::tl -> begin
 (
 
-let _63_1110 = (pop_record_cache ())
+let _63_1242 = (pop_record_cache ())
 in (
 
-let _63_1112 = (FStar_ST.op_Colon_Equals stack tl)
+let _63_1244 = (FStar_ST.op_Colon_Equals stack tl)
 in env))
 end
-| _63_1115 -> begin
+| _63_1247 -> begin
 (FStar_All.failwith "Impossible: Too many pops")
 end))
 in (
 
 let commit_mark = (fun env -> (
 
-let _63_1118 = (commit_record_cache ())
+let _63_1250 = (commit_record_cache ())
 in (match ((FStar_ST.read stack)) with
-| (_63_1122)::tl -> begin
+| (_63_1254)::tl -> begin
 (
 
-let _63_1124 = (FStar_ST.op_Colon_Equals stack tl)
+let _63_1256 = (FStar_ST.op_Colon_Equals stack tl)
 in env)
 end
-| _63_1127 -> begin
+| _63_1259 -> begin
 (FStar_All.failwith "Impossible: Too many pops")
 end)))
 in {push = push; mark = push; reset_mark = pop; commit_mark = commit_mark; pop = pop}))))
@@ -1485,10 +1829,10 @@ let pop : env  ->  env = (fun env -> (stack_ops.pop env))
 let export_interface : FStar_Ident.lident  ->  env  ->  env = (fun m env -> (
 
 let sigelt_in_m = (fun se -> (match ((FStar_Syntax_Util.lids_of_sigelt se)) with
-| (l)::_63_1138 -> begin
+| (l)::_63_1270 -> begin
 (l.FStar_Ident.nsstr = m.FStar_Ident.str)
 end
-| _63_1142 -> begin
+| _63_1274 -> begin
 false
 end))
 in (
@@ -1505,23 +1849,23 @@ in (
 let sm' = (sigmap env)
 in (
 
-let _63_1166 = (FStar_All.pipe_right keys (FStar_List.iter (fun k -> (match ((FStar_Util.smap_try_find sm' k)) with
+let _63_1298 = (FStar_All.pipe_right keys (FStar_List.iter (fun k -> (match ((FStar_Util.smap_try_find sm' k)) with
 | Some (se, true) when (sigelt_in_m se) -> begin
 (
 
-let _63_1152 = (FStar_Util.smap_remove sm' k)
+let _63_1284 = (FStar_Util.smap_remove sm' k)
 in (
 
 let se = (match (se) with
 | FStar_Syntax_Syntax.Sig_declare_typ (l, u, t, q, r) -> begin
 FStar_Syntax_Syntax.Sig_declare_typ (((l), (u), (t), ((FStar_Syntax_Syntax.Assumption)::q), (r)))
 end
-| _63_1162 -> begin
+| _63_1294 -> begin
 se
 end)
 in (FStar_Util.smap_add sm' k ((se), (false)))))
 end
-| _63_1165 -> begin
+| _63_1297 -> begin
 ()
 end))))
 in env)))))))
@@ -1529,7 +1873,7 @@ in env)))))))
 
 let finish_module_or_interface : env  ->  FStar_Syntax_Syntax.modul  ->  env = (fun env modul -> (
 
-let _63_1170 = if (not (modul.FStar_Syntax_Syntax.is_interface)) then begin
+let _63_1302 = if (not (modul.FStar_Syntax_Syntax.is_interface)) then begin
 (check_admits env)
 end else begin
 ()
@@ -1562,35 +1906,56 @@ open_ns
 end
 in (
 
-let _63_1181 = env
-in (let _158_903 = (FStar_List.map (fun lid -> Open_module_or_namespace (((lid), (Open_namespace)))) open_ns)
-in {curmodule = Some (mname); curmonad = _63_1181.curmonad; modules = _63_1181.modules; scope_mods = _158_903; sigaccum = _63_1181.sigaccum; sigmap = env.sigmap; default_result_effect = if ((FStar_Ident.lid_equals mname FStar_Syntax_Const.all_lid) || (has_all_in_scope env)) then begin
+let _63_1313 = (let _158_1042 = (exported_id_set_new ())
+in (FStar_Util.smap_add env.exported_ids mname.FStar_Ident.str _158_1042))
+in (match (()) with
+| () -> begin
+(
+
+let _63_1314 = (let _158_1043 = (exported_id_set_new ())
+in (FStar_Util.smap_add env.trans_exported_ids mname.FStar_Ident.str _158_1043))
+in (match (()) with
+| () -> begin
+(
+
+let _63_1315 = (let _158_1044 = (FStar_Util.mk_ref [])
+in (FStar_Util.smap_add env.includes mname.FStar_Ident.str _158_1044))
+in (match (()) with
+| () -> begin
+(
+
+let _63_1316 = env
+in (let _158_1046 = (FStar_List.map (fun lid -> Open_module_or_namespace (((lid), (Open_namespace)))) open_ns)
+in {curmodule = Some (mname); curmonad = _63_1316.curmonad; modules = _63_1316.modules; scope_mods = _158_1046; exported_ids = _63_1316.exported_ids; trans_exported_ids = _63_1316.trans_exported_ids; includes = _63_1316.includes; sigaccum = _63_1316.sigaccum; sigmap = env.sigmap; default_result_effect = if ((FStar_Ident.lid_equals mname FStar_Syntax_Const.all_lid) || (has_all_in_scope env)) then begin
 FStar_Syntax_Const.effect_ML_lid
 end else begin
 FStar_Syntax_Const.effect_Tot_lid
-end; iface = intf; admitted_iface = admitted; expect_typ = _63_1181.expect_typ})))))
-in (match ((FStar_All.pipe_right env.modules (FStar_Util.find_opt (fun _63_1187 -> (match (_63_1187) with
-| (l, _63_1186) -> begin
+end; iface = intf; admitted_iface = admitted; expect_typ = _63_1316.expect_typ}))
+end))
+end))
+end)))))
+in (match ((FStar_All.pipe_right env.modules (FStar_Util.find_opt (fun _63_1322 -> (match (_63_1322) with
+| (l, _63_1321) -> begin
 (FStar_Ident.lid_equals l mname)
 end))))) with
 | None -> begin
-(let _158_905 = (prep env)
-in ((_158_905), (false)))
+(let _158_1048 = (prep env)
+in ((_158_1048), (false)))
 end
-| Some (_63_1190, m) -> begin
+| Some (_63_1325, m) -> begin
 (
 
-let _63_1194 = if ((not (m.FStar_Syntax_Syntax.is_interface)) || intf) then begin
-(let _158_908 = (let _158_907 = (let _158_906 = (FStar_Util.format1 "Duplicate module or interface name: %s" mname.FStar_Ident.str)
-in ((_158_906), ((FStar_Ident.range_of_lid mname))))
-in FStar_Syntax_Syntax.Error (_158_907))
-in (Prims.raise _158_908))
+let _63_1329 = if ((not (m.FStar_Syntax_Syntax.is_interface)) || intf) then begin
+(let _158_1051 = (let _158_1050 = (let _158_1049 = (FStar_Util.format1 "Duplicate module or interface name: %s" mname.FStar_Ident.str)
+in ((_158_1049), ((FStar_Ident.range_of_lid mname))))
+in FStar_Syntax_Syntax.Error (_158_1050))
+in (Prims.raise _158_1051))
 end else begin
 ()
 end
-in (let _158_910 = (let _158_909 = (push env)
-in (prep _158_909))
-in ((_158_910), (true))))
+in (let _158_1053 = (let _158_1052 = (push env)
+in (prep _158_1052))
+in ((_158_1053), (true))))
 end)))
 
 
@@ -1601,8 +1966,8 @@ end
 | None -> begin
 (
 
-let _63_1201 = env
-in {curmodule = _63_1201.curmodule; curmonad = Some (mname); modules = _63_1201.modules; scope_mods = _63_1201.scope_mods; sigaccum = _63_1201.sigaccum; sigmap = _63_1201.sigmap; default_result_effect = _63_1201.default_result_effect; iface = _63_1201.iface; admitted_iface = _63_1201.admitted_iface; expect_typ = _63_1201.expect_typ})
+let _63_1336 = env
+in {curmodule = _63_1336.curmodule; curmonad = Some (mname); modules = _63_1336.modules; scope_mods = _63_1336.scope_mods; exported_ids = _63_1336.exported_ids; trans_exported_ids = _63_1336.trans_exported_ids; includes = _63_1336.includes; sigaccum = _63_1336.sigaccum; sigmap = _63_1336.sigmap; default_result_effect = _63_1336.default_result_effect; iface = _63_1336.iface; admitted_iface = _63_1336.admitted_iface; expect_typ = _63_1336.expect_typ})
 end))
 
 
@@ -1610,8 +1975,8 @@ let fail_or = (fun env lookup lid -> (match ((lookup lid)) with
 | None -> begin
 (
 
-let opened_modules = (FStar_List.map (fun _63_1210 -> (match (_63_1210) with
-| (lid, _63_1209) -> begin
+let opened_modules = (FStar_List.map (fun _63_1345 -> (match (_63_1345) with
+| (lid, _63_1344) -> begin
 (FStar_Ident.text_of_lid lid)
 end)) env.modules)
 in (
@@ -1624,8 +1989,8 @@ msg
 end else begin
 (
 
-let modul = (let _158_922 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
-in (FStar_Ident.set_lid_range _158_922 (FStar_Ident.range_of_lid lid)))
+let modul = (let _158_1065 = (FStar_Ident.lid_of_ids lid.FStar_Ident.ns)
+in (FStar_Ident.set_lid_range _158_1065 (FStar_Ident.range_of_lid lid)))
 in (match ((resolve_module_name env modul true)) with
 | None -> begin
 (
diff --git a/src/ocaml-output/FStar_Parser_Lexhelp.ml b/src/ocaml-output/FStar_Parser_Lexhelp.ml
index c6ecdeff1b6..51e9083cc13 100755
--- a/src/ocaml-output/FStar_Parser_Lexhelp.ml
+++ b/src/ocaml-output/FStar_Parser_Lexhelp.ml
@@ -191,7 +191,7 @@ false
 end))
 
 
-let keywords : (compatibilityMode * Prims.string * FStar_Parser_Parse.token) Prims.list = (((ALWAYS), ("abstract"), (FStar_Parser_Parse.ABSTRACT)))::(((ALWAYS), ("noeq"), (FStar_Parser_Parse.NOEQUALITY)))::(((ALWAYS), ("unopteq"), (FStar_Parser_Parse.UNOPTEQUALITY)))::(((ALWAYS), ("and"), (FStar_Parser_Parse.AND)))::(((ALWAYS), ("assert"), (FStar_Parser_Parse.ASSERT)))::(((ALWAYS), ("assume"), (FStar_Parser_Parse.ASSUME)))::(((ALWAYS), ("begin"), (FStar_Parser_Parse.BEGIN)))::(((FSHARP), ("default"), (FStar_Parser_Parse.DEFAULT)))::(((ALWAYS), ("effect"), (FStar_Parser_Parse.EFFECT)))::(((ALWAYS), ("effect_actions"), (FStar_Parser_Parse.ACTIONS)))::(((ALWAYS), ("else"), (FStar_Parser_Parse.ELSE)))::(((ALWAYS), ("end"), (FStar_Parser_Parse.END)))::(((ALWAYS), ("ensures"), (FStar_Parser_Parse.ENSURES)))::(((ALWAYS), ("exception"), (FStar_Parser_Parse.EXCEPTION)))::(((ALWAYS), ("exists"), (FStar_Parser_Parse.EXISTS)))::(((ALWAYS), ("false"), (FStar_Parser_Parse.FALSE)))::(((ALWAYS), ("False"), (FStar_Parser_Parse.L_FALSE)))::(((ALWAYS), ("forall"), (FStar_Parser_Parse.FORALL)))::(((ALWAYS), ("fun"), (FStar_Parser_Parse.FUN)))::(((ALWAYS), ("function"), (FStar_Parser_Parse.FUNCTION)))::(((ALWAYS), ("if"), (FStar_Parser_Parse.IF)))::(((ALWAYS), ("kind"), (FStar_Parser_Parse.KIND)))::(((ALWAYS), ("in"), (FStar_Parser_Parse.IN)))::(((ALWAYS), ("inline"), (FStar_Parser_Parse.INLINE)))::(((ALWAYS), ("inline_for_extraction"), (FStar_Parser_Parse.INLINE_FOR_EXTRACTION)))::(((ALWAYS), ("irreducible"), (FStar_Parser_Parse.IRREDUCIBLE)))::(((ALWAYS), ("let"), (FStar_Parser_Parse.LET (false))))::(((ALWAYS), ("logic"), (FStar_Parser_Parse.LOGIC)))::(((ALWAYS), ("match"), (FStar_Parser_Parse.MATCH)))::(((ALWAYS), ("module"), (FStar_Parser_Parse.MODULE)))::(((ALWAYS), ("mutable"), (FStar_Parser_Parse.MUTABLE)))::(((ALWAYS), ("new"), (FStar_Parser_Parse.NEW)))::(((ALWAYS), ("new_effect"), (FStar_Parser_Parse.NEW_EFFECT)))::(((ALWAYS), ("new_effect_for_free"), (FStar_Parser_Parse.NEW_EFFECT_FOR_FREE)))::(((ALWAYS), ("noextract"), (FStar_Parser_Parse.NOEXTRACT)))::(((ALWAYS), ("of"), (FStar_Parser_Parse.OF)))::(((ALWAYS), ("open"), (FStar_Parser_Parse.OPEN)))::(((ALWAYS), ("opaque"), (FStar_Parser_Parse.OPAQUE)))::(((ALWAYS), ("private"), (FStar_Parser_Parse.PRIVATE)))::(((ALWAYS), ("rec"), (FStar_Parser_Parse.REC)))::(((ALWAYS), ("reifiable"), (FStar_Parser_Parse.REIFIABLE)))::(((ALWAYS), ("reify"), (FStar_Parser_Parse.REIFY)))::(((ALWAYS), ("reflectable"), (FStar_Parser_Parse.REFLECTABLE)))::(((ALWAYS), ("requires"), (FStar_Parser_Parse.REQUIRES)))::(((ALWAYS), ("sub_effect"), (FStar_Parser_Parse.SUB_EFFECT)))::(((ALWAYS), ("then"), (FStar_Parser_Parse.THEN)))::(((ALWAYS), ("total"), (FStar_Parser_Parse.TOTAL)))::(((ALWAYS), ("true"), (FStar_Parser_Parse.TRUE)))::(((ALWAYS), ("True"), (FStar_Parser_Parse.L_TRUE)))::(((ALWAYS), ("try"), (FStar_Parser_Parse.TRY)))::(((ALWAYS), ("type"), (FStar_Parser_Parse.TYPE)))::(((ALWAYS), ("unfold"), (FStar_Parser_Parse.UNFOLD)))::(((ALWAYS), ("unfoldable"), (FStar_Parser_Parse.UNFOLDABLE)))::(((ALWAYS), ("val"), (FStar_Parser_Parse.VAL)))::(((ALWAYS), ("when"), (FStar_Parser_Parse.WHEN)))::(((ALWAYS), ("with"), (FStar_Parser_Parse.WITH)))::(((ALWAYS), ("_"), (FStar_Parser_Parse.UNDERSCORE)))::[]
+let keywords : (compatibilityMode * Prims.string * FStar_Parser_Parse.token) Prims.list = (((ALWAYS), ("abstract"), (FStar_Parser_Parse.ABSTRACT)))::(((ALWAYS), ("noeq"), (FStar_Parser_Parse.NOEQUALITY)))::(((ALWAYS), ("unopteq"), (FStar_Parser_Parse.UNOPTEQUALITY)))::(((ALWAYS), ("and"), (FStar_Parser_Parse.AND)))::(((ALWAYS), ("assert"), (FStar_Parser_Parse.ASSERT)))::(((ALWAYS), ("assume"), (FStar_Parser_Parse.ASSUME)))::(((ALWAYS), ("begin"), (FStar_Parser_Parse.BEGIN)))::(((FSHARP), ("default"), (FStar_Parser_Parse.DEFAULT)))::(((ALWAYS), ("effect"), (FStar_Parser_Parse.EFFECT)))::(((ALWAYS), ("effect_actions"), (FStar_Parser_Parse.ACTIONS)))::(((ALWAYS), ("else"), (FStar_Parser_Parse.ELSE)))::(((ALWAYS), ("end"), (FStar_Parser_Parse.END)))::(((ALWAYS), ("ensures"), (FStar_Parser_Parse.ENSURES)))::(((ALWAYS), ("exception"), (FStar_Parser_Parse.EXCEPTION)))::(((ALWAYS), ("exists"), (FStar_Parser_Parse.EXISTS)))::(((ALWAYS), ("false"), (FStar_Parser_Parse.FALSE)))::(((ALWAYS), ("False"), (FStar_Parser_Parse.L_FALSE)))::(((ALWAYS), ("forall"), (FStar_Parser_Parse.FORALL)))::(((ALWAYS), ("fun"), (FStar_Parser_Parse.FUN)))::(((ALWAYS), ("function"), (FStar_Parser_Parse.FUNCTION)))::(((ALWAYS), ("if"), (FStar_Parser_Parse.IF)))::(((ALWAYS), ("kind"), (FStar_Parser_Parse.KIND)))::(((ALWAYS), ("in"), (FStar_Parser_Parse.IN)))::(((ALWAYS), ("include"), (FStar_Parser_Parse.INCLUDE)))::(((ALWAYS), ("inline"), (FStar_Parser_Parse.INLINE)))::(((ALWAYS), ("inline_for_extraction"), (FStar_Parser_Parse.INLINE_FOR_EXTRACTION)))::(((ALWAYS), ("irreducible"), (FStar_Parser_Parse.IRREDUCIBLE)))::(((ALWAYS), ("let"), (FStar_Parser_Parse.LET (false))))::(((ALWAYS), ("logic"), (FStar_Parser_Parse.LOGIC)))::(((ALWAYS), ("match"), (FStar_Parser_Parse.MATCH)))::(((ALWAYS), ("module"), (FStar_Parser_Parse.MODULE)))::(((ALWAYS), ("mutable"), (FStar_Parser_Parse.MUTABLE)))::(((ALWAYS), ("new"), (FStar_Parser_Parse.NEW)))::(((ALWAYS), ("new_effect"), (FStar_Parser_Parse.NEW_EFFECT)))::(((ALWAYS), ("new_effect_for_free"), (FStar_Parser_Parse.NEW_EFFECT_FOR_FREE)))::(((ALWAYS), ("noextract"), (FStar_Parser_Parse.NOEXTRACT)))::(((ALWAYS), ("of"), (FStar_Parser_Parse.OF)))::(((ALWAYS), ("open"), (FStar_Parser_Parse.OPEN)))::(((ALWAYS), ("opaque"), (FStar_Parser_Parse.OPAQUE)))::(((ALWAYS), ("private"), (FStar_Parser_Parse.PRIVATE)))::(((ALWAYS), ("rec"), (FStar_Parser_Parse.REC)))::(((ALWAYS), ("reifiable"), (FStar_Parser_Parse.REIFIABLE)))::(((ALWAYS), ("reify"), (FStar_Parser_Parse.REIFY)))::(((ALWAYS), ("reflectable"), (FStar_Parser_Parse.REFLECTABLE)))::(((ALWAYS), ("requires"), (FStar_Parser_Parse.REQUIRES)))::(((ALWAYS), ("sub_effect"), (FStar_Parser_Parse.SUB_EFFECT)))::(((ALWAYS), ("then"), (FStar_Parser_Parse.THEN)))::(((ALWAYS), ("total"), (FStar_Parser_Parse.TOTAL)))::(((ALWAYS), ("true"), (FStar_Parser_Parse.TRUE)))::(((ALWAYS), ("True"), (FStar_Parser_Parse.L_TRUE)))::(((ALWAYS), ("try"), (FStar_Parser_Parse.TRY)))::(((ALWAYS), ("type"), (FStar_Parser_Parse.TYPE)))::(((ALWAYS), ("unfold"), (FStar_Parser_Parse.UNFOLD)))::(((ALWAYS), ("unfoldable"), (FStar_Parser_Parse.UNFOLDABLE)))::(((ALWAYS), ("val"), (FStar_Parser_Parse.VAL)))::(((ALWAYS), ("when"), (FStar_Parser_Parse.WHEN)))::(((ALWAYS), ("with"), (FStar_Parser_Parse.WITH)))::(((ALWAYS), ("_"), (FStar_Parser_Parse.UNDERSCORE)))::[]
 
 
 let stringKeywords : Prims.string Prims.list = (FStar_List.map (fun _67_61 -> (match (_67_61) with
diff --git a/src/ocaml-output/FStar_Parser_ToSyntax.ml b/src/ocaml-output/FStar_Parser_ToSyntax.ml
index 89ec5f2fa0b..cb74cf196d9 100755
--- a/src/ocaml-output/FStar_Parser_ToSyntax.ml
+++ b/src/ocaml-output/FStar_Parser_ToSyntax.ml
@@ -1157,14 +1157,14 @@ and desugar_term : FStar_Parser_Env.env  ->  FStar_Parser_AST.term  ->  FStar_Sy
 let env = (
 
 let _65_879 = env
-in {FStar_Parser_Env.curmodule = _65_879.FStar_Parser_Env.curmodule; FStar_Parser_Env.curmonad = _65_879.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_879.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_879.FStar_Parser_Env.scope_mods; FStar_Parser_Env.sigaccum = _65_879.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_879.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_879.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_879.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_879.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = false})
+in {FStar_Parser_Env.curmodule = _65_879.FStar_Parser_Env.curmodule; FStar_Parser_Env.curmonad = _65_879.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_879.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_879.FStar_Parser_Env.scope_mods; FStar_Parser_Env.exported_ids = _65_879.FStar_Parser_Env.exported_ids; FStar_Parser_Env.trans_exported_ids = _65_879.FStar_Parser_Env.trans_exported_ids; FStar_Parser_Env.includes = _65_879.FStar_Parser_Env.includes; FStar_Parser_Env.sigaccum = _65_879.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_879.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_879.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_879.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_879.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = false})
 in (desugar_term_maybe_top false env e)))
 and desugar_typ : FStar_Parser_Env.env  ->  FStar_Parser_AST.term  ->  FStar_Syntax_Syntax.term = (fun env e -> (
 
 let env = (
 
 let _65_884 = env
-in {FStar_Parser_Env.curmodule = _65_884.FStar_Parser_Env.curmodule; FStar_Parser_Env.curmonad = _65_884.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_884.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_884.FStar_Parser_Env.scope_mods; FStar_Parser_Env.sigaccum = _65_884.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_884.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_884.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_884.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_884.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = true})
+in {FStar_Parser_Env.curmodule = _65_884.FStar_Parser_Env.curmodule; FStar_Parser_Env.curmonad = _65_884.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_884.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_884.FStar_Parser_Env.scope_mods; FStar_Parser_Env.exported_ids = _65_884.FStar_Parser_Env.exported_ids; FStar_Parser_Env.trans_exported_ids = _65_884.FStar_Parser_Env.trans_exported_ids; FStar_Parser_Env.includes = _65_884.FStar_Parser_Env.includes; FStar_Parser_Env.sigaccum = _65_884.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_884.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_884.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_884.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_884.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = true})
 in (desugar_term_maybe_top false env e)))
 and desugar_machine_integer : FStar_Parser_Env.env  ->  Prims.string  ->  (FStar_Const.signedness * FStar_Const.width)  ->  FStar_Range.range  ->  (FStar_Syntax_Syntax.term', FStar_Syntax_Syntax.term') FStar_Syntax_Syntax.syntax = (fun env repr _65_891 range -> (match (_65_891) with
 | (signedness, width) -> begin
@@ -3825,6 +3825,12 @@ end
 let env = (FStar_Parser_Env.push_namespace env lid)
 in ((env), ([])))
 end
+| FStar_Parser_AST.Include (lid) -> begin
+(
+
+let env = (FStar_Parser_Env.push_include env lid)
+in ((env), ([])))
+end
 | FStar_Parser_AST.ModuleAbbrev (x, l) -> begin
 (let _160_1100 = (FStar_Parser_Env.push_module_abbrev env x l)
 in ((_160_1100), ([])))
@@ -3832,8 +3838,8 @@ end
 | FStar_Parser_AST.Tycon (qual, tcs) -> begin
 (
 
-let tcs = (FStar_List.map (fun _65_2739 -> (match (_65_2739) with
-| (x, _65_2738) -> begin
+let tcs = (FStar_List.map (fun _65_2742 -> (match (_65_2742) with
+| (x, _65_2741) -> begin
 x
 end)) tcs)
 in (let _160_1102 = (FStar_List.map (trans_qual None) qual)
@@ -3843,29 +3849,29 @@ end
 (match ((let _160_1104 = (let _160_1103 = (desugar_term_maybe_top true env (FStar_Parser_AST.mk_term (FStar_Parser_AST.Let (((isrec), (lets), ((FStar_Parser_AST.mk_term (FStar_Parser_AST.Const (FStar_Const.Const_unit)) d.FStar_Parser_AST.drange FStar_Parser_AST.Expr))))) d.FStar_Parser_AST.drange FStar_Parser_AST.Expr))
 in (FStar_All.pipe_left FStar_Syntax_Subst.compress _160_1103))
 in _160_1104.FStar_Syntax_Syntax.n)) with
-| FStar_Syntax_Syntax.Tm_let (lbs, _65_2748) -> begin
+| FStar_Syntax_Syntax.Tm_let (lbs, _65_2751) -> begin
 (
 
 let fvs = (FStar_All.pipe_right (Prims.snd lbs) (FStar_List.map (fun lb -> (FStar_Util.right lb.FStar_Syntax_Syntax.lbname))))
 in (
 
 let quals = (match (quals) with
-| (_65_2756)::_65_2754 -> begin
+| (_65_2759)::_65_2757 -> begin
 (FStar_List.map (trans_qual None) quals)
 end
-| _65_2759 -> begin
+| _65_2762 -> begin
 (FStar_All.pipe_right (Prims.snd lbs) (FStar_List.collect (fun _65_25 -> (match (_65_25) with
-| {FStar_Syntax_Syntax.lbname = FStar_Util.Inl (_65_2770); FStar_Syntax_Syntax.lbunivs = _65_2768; FStar_Syntax_Syntax.lbtyp = _65_2766; FStar_Syntax_Syntax.lbeff = _65_2764; FStar_Syntax_Syntax.lbdef = _65_2762} -> begin
+| {FStar_Syntax_Syntax.lbname = FStar_Util.Inl (_65_2773); FStar_Syntax_Syntax.lbunivs = _65_2771; FStar_Syntax_Syntax.lbtyp = _65_2769; FStar_Syntax_Syntax.lbeff = _65_2767; FStar_Syntax_Syntax.lbdef = _65_2765} -> begin
 []
 end
-| {FStar_Syntax_Syntax.lbname = FStar_Util.Inr (fv); FStar_Syntax_Syntax.lbunivs = _65_2780; FStar_Syntax_Syntax.lbtyp = _65_2778; FStar_Syntax_Syntax.lbeff = _65_2776; FStar_Syntax_Syntax.lbdef = _65_2774} -> begin
+| {FStar_Syntax_Syntax.lbname = FStar_Util.Inr (fv); FStar_Syntax_Syntax.lbunivs = _65_2783; FStar_Syntax_Syntax.lbtyp = _65_2781; FStar_Syntax_Syntax.lbeff = _65_2779; FStar_Syntax_Syntax.lbdef = _65_2777} -> begin
 (FStar_Parser_Env.lookup_letbinding_quals env fv.FStar_Syntax_Syntax.fv_name.FStar_Syntax_Syntax.v)
 end))))
 end)
 in (
 
-let quals = if (FStar_All.pipe_right lets (FStar_Util.for_some (fun _65_2788 -> (match (_65_2788) with
-| (_65_2786, t) -> begin
+let quals = if (FStar_All.pipe_right lets (FStar_Util.for_some (fun _65_2791 -> (match (_65_2791) with
+| (_65_2789, t) -> begin
 (t.FStar_Parser_AST.level = FStar_Parser_AST.Formula)
 end)))) then begin
 (FStar_Syntax_Syntax.Logic)::quals
@@ -3880,11 +3886,11 @@ let lbs = if (FStar_All.pipe_right quals (FStar_List.contains FStar_Syntax_Synta
 let fv = (FStar_Util.right lb.FStar_Syntax_Syntax.lbname)
 in (
 
-let _65_2792 = lb
+let _65_2795 = lb
 in {FStar_Syntax_Syntax.lbname = FStar_Util.Inr ((
 
-let _65_2794 = fv
-in {FStar_Syntax_Syntax.fv_name = _65_2794.FStar_Syntax_Syntax.fv_name; FStar_Syntax_Syntax.fv_delta = FStar_Syntax_Syntax.Delta_abstract (fv.FStar_Syntax_Syntax.fv_delta); FStar_Syntax_Syntax.fv_qual = _65_2794.FStar_Syntax_Syntax.fv_qual})); FStar_Syntax_Syntax.lbunivs = _65_2792.FStar_Syntax_Syntax.lbunivs; FStar_Syntax_Syntax.lbtyp = _65_2792.FStar_Syntax_Syntax.lbtyp; FStar_Syntax_Syntax.lbeff = _65_2792.FStar_Syntax_Syntax.lbeff; FStar_Syntax_Syntax.lbdef = _65_2792.FStar_Syntax_Syntax.lbdef})))))
+let _65_2797 = fv
+in {FStar_Syntax_Syntax.fv_name = _65_2797.FStar_Syntax_Syntax.fv_name; FStar_Syntax_Syntax.fv_delta = FStar_Syntax_Syntax.Delta_abstract (fv.FStar_Syntax_Syntax.fv_delta); FStar_Syntax_Syntax.fv_qual = _65_2797.FStar_Syntax_Syntax.fv_qual})); FStar_Syntax_Syntax.lbunivs = _65_2795.FStar_Syntax_Syntax.lbunivs; FStar_Syntax_Syntax.lbtyp = _65_2795.FStar_Syntax_Syntax.lbtyp; FStar_Syntax_Syntax.lbeff = _65_2795.FStar_Syntax_Syntax.lbeff; FStar_Syntax_Syntax.lbdef = _65_2795.FStar_Syntax_Syntax.lbdef})))))
 in (((Prims.fst lbs)), (_160_1109)))
 end else begin
 lbs
@@ -3899,7 +3905,7 @@ in (
 let env = (FStar_Parser_Env.push_sigelt env s)
 in ((env), ((s)::[]))))))))
 end
-| _65_2801 -> begin
+| _65_2804 -> begin
 (FStar_All.failwith "Desugaring a let did not produce a let")
 end)
 end
@@ -3948,9 +3954,9 @@ end
 | FStar_Parser_AST.Exception (id, None) -> begin
 (
 
-let _65_2828 = (FStar_Parser_Env.fail_or env (FStar_Parser_Env.try_lookup_lid env) FStar_Syntax_Const.exn_lid)
-in (match (_65_2828) with
-| (t, _65_2827) -> begin
+let _65_2831 = (FStar_Parser_Env.fail_or env (FStar_Parser_Env.try_lookup_lid env) FStar_Syntax_Const.exn_lid)
+in (match (_65_2831) with
+| (t, _65_2830) -> begin
 (
 
 let l = (FStar_Parser_Env.qualify env id)
@@ -4013,8 +4019,8 @@ end
 | FStar_Parser_AST.KindAbbrev (id, binders, k) -> begin
 (
 
-let _65_2857 = (desugar_binders env binders)
-in (match (_65_2857) with
+let _65_2860 = (desugar_binders env binders)
+in (match (_65_2860) with
 | (env_k, binders) -> begin
 (
 
@@ -4066,7 +4072,7 @@ in (
 let dst = (lookup l.FStar_Parser_AST.mdest)
 in (
 
-let _65_2921 = (match (l.FStar_Parser_AST.lift_op) with
+let _65_2924 = (match (l.FStar_Parser_AST.lift_op) with
 | FStar_Parser_AST.NonReifiableLift (t) -> begin
 (let _160_1139 = (let _160_1138 = (let _160_1137 = (desugar_term env t)
 in (([]), (_160_1137)))
@@ -4088,7 +4094,7 @@ in (([]), (_160_1146)))
 in Some (_160_1147))
 in ((None), (_160_1148)))
 end)
-in (match (_65_2921) with
+in (match (_65_2924) with
 | (lift_wp, lift) -> begin
 (
 
@@ -4098,12 +4104,12 @@ end)))))
 end)))
 
 
-let desugar_decls : FStar_Parser_Env.env  ->  FStar_Parser_AST.decl Prims.list  ->  (FStar_Parser_Env.env * FStar_Syntax_Syntax.sigelts) = (fun env decls -> (FStar_List.fold_left (fun _65_2927 d -> (match (_65_2927) with
+let desugar_decls : FStar_Parser_Env.env  ->  FStar_Parser_AST.decl Prims.list  ->  (FStar_Parser_Env.env * FStar_Syntax_Syntax.sigelts) = (fun env decls -> (FStar_List.fold_left (fun _65_2930 d -> (match (_65_2930) with
 | (env, sigelts) -> begin
 (
 
-let _65_2931 = (desugar_decl env d)
-in (match (_65_2931) with
+let _65_2934 = (desugar_decl env d)
+in (match (_65_2934) with
 | (env, se) -> begin
 ((env), ((FStar_List.append sigelts se)))
 end))
@@ -4124,7 +4130,7 @@ end
 end)
 in (
 
-let _65_2954 = (match (m) with
+let _65_2957 = (match (m) with
 | FStar_Parser_AST.Interface (mname, decls, admitted) -> begin
 (let _160_1166 = (FStar_Parser_Env.prepare_module_or_interface true admitted env mname)
 in ((_160_1166), (mname), (decls), (true)))
@@ -4133,12 +4139,12 @@ end
 (let _160_1167 = (FStar_Parser_Env.prepare_module_or_interface false false env mname)
 in ((_160_1167), (mname), (decls), (false)))
 end)
-in (match (_65_2954) with
+in (match (_65_2957) with
 | ((env, pop_when_done), mname, decls, intf) -> begin
 (
 
-let _65_2957 = (desugar_decls env decls)
-in (match (_65_2957) with
+let _65_2960 = (desugar_decls env decls)
+in (match (_65_2960) with
 | (env, sigelts) -> begin
 (
 
@@ -4155,7 +4161,7 @@ let m = if (FStar_Options.interactive_fsi ()) then begin
 | FStar_Parser_AST.Module (mname, decls) -> begin
 FStar_Parser_AST.Interface (((mname), (decls), (true)))
 end
-| FStar_Parser_AST.Interface (mname, _65_2968, _65_2970) -> begin
+| FStar_Parser_AST.Interface (mname, _65_2971, _65_2973) -> begin
 (FStar_All.failwith (Prims.strcat "Impossible: " mname.FStar_Ident.ident.FStar_Ident.idText))
 end)
 end else begin
@@ -4163,24 +4169,24 @@ m
 end
 in (
 
-let _65_2978 = (desugar_modul_common curmod env m)
-in (match (_65_2978) with
-| (x, y, _65_2977) -> begin
+let _65_2981 = (desugar_modul_common curmod env m)
+in (match (_65_2981) with
+| (x, y, _65_2980) -> begin
 ((x), (y))
 end))))
 
 
 let desugar_modul : FStar_Parser_Env.env  ->  FStar_Parser_AST.modul  ->  (env_t * FStar_Syntax_Syntax.modul) = (fun env m -> (
 
-let _65_2984 = (desugar_modul_common None env m)
-in (match (_65_2984) with
+let _65_2987 = (desugar_modul_common None env m)
+in (match (_65_2987) with
 | (env, modul, pop_when_done) -> begin
 (
 
 let env = (FStar_Parser_Env.finish_module_or_interface env modul)
 in (
 
-let _65_2986 = if (FStar_Options.dump_module modul.FStar_Syntax_Syntax.name.FStar_Ident.str) then begin
+let _65_2989 = if (FStar_Options.dump_module modul.FStar_Syntax_Syntax.name.FStar_Ident.str) then begin
 (let _160_1178 = (FStar_Syntax_Print.modul_to_string modul)
 in (FStar_Util.print1 "%s\n" _160_1178))
 end else begin
@@ -4197,17 +4203,17 @@ end)))
 
 let desugar_file : FStar_Parser_Env.env  ->  FStar_Parser_AST.file  ->  (FStar_Parser_Env.env * FStar_Syntax_Syntax.modul Prims.list) = (fun env f -> (
 
-let _65_2999 = (FStar_List.fold_left (fun _65_2992 m -> (match (_65_2992) with
+let _65_3002 = (FStar_List.fold_left (fun _65_2995 m -> (match (_65_2995) with
 | (env, mods) -> begin
 (
 
-let _65_2996 = (desugar_modul env m)
-in (match (_65_2996) with
+let _65_2999 = (desugar_modul env m)
+in (match (_65_2999) with
 | (env, m) -> begin
 ((env), ((m)::mods))
 end))
 end)) ((env), ([])) f)
-in (match (_65_2999) with
+in (match (_65_3002) with
 | (env, mods) -> begin
 ((env), ((FStar_List.rev mods)))
 end)))
@@ -4215,15 +4221,15 @@ end)))
 
 let add_modul_to_env : FStar_Syntax_Syntax.modul  ->  FStar_Parser_Env.env  ->  FStar_Parser_Env.env = (fun m en -> (
 
-let _65_3004 = (FStar_Parser_Env.prepare_module_or_interface false false en m.FStar_Syntax_Syntax.name)
-in (match (_65_3004) with
+let _65_3007 = (FStar_Parser_Env.prepare_module_or_interface false false en m.FStar_Syntax_Syntax.name)
+in (match (_65_3007) with
 | (en, pop_when_done) -> begin
 (
 
 let en = (FStar_List.fold_left FStar_Parser_Env.push_sigelt (
 
-let _65_3005 = en
-in {FStar_Parser_Env.curmodule = Some (m.FStar_Syntax_Syntax.name); FStar_Parser_Env.curmonad = _65_3005.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_3005.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_3005.FStar_Parser_Env.scope_mods; FStar_Parser_Env.sigaccum = _65_3005.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_3005.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_3005.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_3005.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_3005.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = _65_3005.FStar_Parser_Env.expect_typ}) m.FStar_Syntax_Syntax.exports)
+let _65_3008 = en
+in {FStar_Parser_Env.curmodule = Some (m.FStar_Syntax_Syntax.name); FStar_Parser_Env.curmonad = _65_3008.FStar_Parser_Env.curmonad; FStar_Parser_Env.modules = _65_3008.FStar_Parser_Env.modules; FStar_Parser_Env.scope_mods = _65_3008.FStar_Parser_Env.scope_mods; FStar_Parser_Env.exported_ids = _65_3008.FStar_Parser_Env.exported_ids; FStar_Parser_Env.trans_exported_ids = _65_3008.FStar_Parser_Env.trans_exported_ids; FStar_Parser_Env.includes = _65_3008.FStar_Parser_Env.includes; FStar_Parser_Env.sigaccum = _65_3008.FStar_Parser_Env.sigaccum; FStar_Parser_Env.sigmap = _65_3008.FStar_Parser_Env.sigmap; FStar_Parser_Env.default_result_effect = _65_3008.FStar_Parser_Env.default_result_effect; FStar_Parser_Env.iface = _65_3008.FStar_Parser_Env.iface; FStar_Parser_Env.admitted_iface = _65_3008.FStar_Parser_Env.admitted_iface; FStar_Parser_Env.expect_typ = _65_3008.FStar_Parser_Env.expect_typ}) m.FStar_Syntax_Syntax.exports)
 in (
 
 let env = (FStar_Parser_Env.finish_module_or_interface en m)
diff --git a/src/parser/ast.fs b/src/parser/ast.fs
index 65ffe3ba52a..a7224464dd6 100644
--- a/src/parser/ast.fs
+++ b/src/parser/ast.fs
@@ -170,6 +170,7 @@ type pragma =
 type decl' =
   | TopLevelModule of lid
   | Open of lid
+  | Include of lid
   | ModuleAbbrev of ident * lid
   | KindAbbrev of ident * list<binder> * knd
   | TopLevelLet of qualifiers * let_qualifier * list<(pattern * term)>
@@ -495,6 +496,7 @@ let id_of_tycon = function
 let decl_to_string (d:decl) = match d.d with
   | TopLevelModule l -> "module " ^ l.str
   | Open l -> "open " ^ l.str
+  | Include l -> "include " ^ l.str
   | ModuleAbbrev (i, l) -> Util.format2 "module %s = %s" i.idText l.str
   | KindAbbrev(i, _, _) -> "kind " ^ i.idText
   | TopLevelLet(_, _, pats) -> "let " ^ (lids_of_let pats |> List.map (fun l -> l.str) |> String.concat ", ")
diff --git a/src/parser/dep.fs b/src/parser/dep.fs
index 246fb65b2b5..b120c961736 100644
--- a/src/parser/dep.fs
+++ b/src/parser/dep.fs
@@ -302,6 +302,7 @@ let collect_one (verify_flags: list<(string * ref<bool>)>) (verify_mode: verify_
     List.iter (fun x -> collect_decl x.d) decls
 
   and collect_decl = function
+    | Include lid
     | Open lid ->
         record_open false lid
     | ModuleAbbrev (ident, lid) ->
diff --git a/src/parser/desugar.fs b/src/parser/desugar.fs
index 534536aac55..eb2cbdf44a7 100644
--- a/src/parser/desugar.fs
+++ b/src/parser/desugar.fs
@@ -1539,6 +1539,9 @@ let rec desugar_decl env (d:decl) : (env_t * sigelts) =
     let env = DesugarEnv.push_namespace env lid in
     env, []
 
+  | Include _ ->
+      failwith "include not supported by legacy desugaring"
+
   | ModuleAbbrev(x, l) -> 
     DesugarEnv.push_module_abbrev env x l, []
 
diff --git a/src/parser/env.fs b/src/parser/env.fs
index 8812b6531f3..627df28ea15 100644
--- a/src/parser/env.fs
+++ b/src/parser/env.fs
@@ -57,11 +57,33 @@ type scope_mod =
 | Top_level_def            of ident           (* top-level definition for an unqualified identifier x to be resolved as curmodule.x. *)
 | Record_or_dc             of record_or_dc    (* to honor interleavings of "open" and record definitions *)
 
+type string_set = set<string>
+
+type exported_id_kind = (* kinds of identifiers exported by a module *)
+| Exported_id_term_type (* term and type identifiers *)
+| Exported_id_field     (* field identifiers *)
+type exported_id_set = exported_id_kind -> ref<string_set>
+
 type env = {
   curmodule:            option<lident>;                   (* name of the module being desugared *)
   curmonad:             option<ident>;                    (* current monad being desugared *)
   modules:              list<(lident * modul)>;           (* previously desugared modules *)
   scope_mods:           list<scope_mod>;                  (* toplevel or definition-local scope modifiers *)
+  exported_ids:         Util.smap<exported_id_set>;       (* identifiers (stored as strings for efficiency)
+                                                             reachable in a module, not shadowed by "include"
+                                                             declarations. Used only to handle such shadowings,
+                                                             not "private"/"abstract" definitions which it is
+                                                             enough to just remove from the sigmap. Formally,
+                                                             iden is in exported_ids[ModulA] if, and only if,
+                                                             there is no 'include ModulB' (with ModulB.iden
+                                                             defined or reachable) after iden in ModulA.
+                                                           *)
+  trans_exported_ids:   Util.smap<exported_id_set>;       (* transitive version of exported_ids along the
+                                                             "include" relation: an identifier is in this set
+                                                             for a module if and only if it is defined either
+                                                             in this module or in one of its included modules.
+                                                           *)
+  includes:             Util.smap<(ref<(list<lident>)>)>; (* list of "includes" declarations for each module. *)
   sigaccum:             sigelts;                          (* type declarations being accumulated for the current module *)
   sigmap:               Util.smap<(sigelt * bool)>;       (* bool indicates that this was declared in an interface file *)
   default_result_effect:lident;                           (* either Tot or ML, depending on the what kind of term we're desugaring *)
@@ -76,6 +98,8 @@ type foundname =
 
 // VALS_HACK_HERE
 
+let all_exported_id_kinds: list<exported_id_kind> = [ Exported_id_field; Exported_id_term_type ]
+
 let open_modules e = e.modules
 let current_module env = match env.curmodule with
     | None -> failwith "Unset current module"
@@ -90,6 +114,9 @@ let empty_env () = {curmodule=None;
                     curmonad=None;
                     modules=[];
                     scope_mods=[];
+                    exported_ids=new_sigmap();
+                    trans_exported_ids=new_sigmap();
+                    includes=new_sigmap();
                     sigaccum=[];
                     sigmap=new_sigmap();
                     default_result_effect=Const.effect_Tot_lid;
@@ -159,9 +186,61 @@ let find_in_record ns id record cont =
       | Some r -> cont r
       | None -> Cont_ignore
 
+let get_exported_id_set (e: env) (mname: string) : option<(exported_id_kind -> ref<string_set>)> =
+    Util.smap_try_find e.exported_ids mname
+
+let get_trans_exported_id_set (e: env) (mname: string) : option<(exported_id_kind -> ref<string_set>)> =
+    Util.smap_try_find e.trans_exported_ids mname
+
+let string_of_exported_id_kind = function
+    | Exported_id_field -> "field"
+    | Exported_id_term_type -> "term/type"
+
+let find_in_module_with_includes
+    (eikind: exported_id_kind)
+    (find_in_module: lident -> cont_t<'a>)
+    (find_in_module_default: cont_t<'a>)
+    env
+    (ns: lident)
+    (id: ident)
+    : cont_t<'a> =
+  let idstr = id.idText in
+  let rec aux = function
+  | [] ->
+    find_in_module_default
+  | modul :: q ->
+    let mname = modul.str in
+    let not_shadowed = match get_exported_id_set env mname with
+    | None -> true
+    | Some mex ->
+      let mexports = !(mex eikind) in
+      Util.set_mem idstr mexports
+    in
+    let mincludes = match Util.smap_try_find env.includes mname with
+    | None -> []
+    | Some minc -> !minc
+    in
+    let look_into =
+     if not_shadowed
+     then find_in_module (qual modul id)
+     else Cont_ignore
+    in
+    begin match look_into with
+    | Cont_ignore ->
+      aux (mincludes @ q)
+    | _ ->
+      look_into
+    end
+  in aux [ ns ]
+
+let is_exported_id_field = function
+  | Exported_id_field -> true
+  | _ -> false
+
 let try_lookup_id''
   env
   (id: ident)
+  (eikind: exported_id_kind)
   (k_local_binding: local_binding -> cont_t<'a>)
   (k_rec_binding:   rec_binding   -> cont_t<'a>)
   (k_record: (record_or_dc * fieldname) -> cont_t<'a>)
@@ -185,8 +264,7 @@ let try_lookup_id''
         k_rec_binding r
 
       | Open_module_or_namespace (ns, _) ->
-        let lid = qual ns id in
-        find_in_module lid
+        find_in_module_with_includes eikind find_in_module Cont_ignore env ns id
 
       | Top_level_def id'
         when id'.idText = id.idText ->
@@ -197,8 +275,13 @@ let try_lookup_id''
         [let] not defined yet, so we must not fail, but ignore. *)
         lookup_default_id Cont_ignore id
 
-      | Record_or_dc r ->
-        find_in_record curmod_ns id r k_record
+      | Record_or_dc r
+        when (is_exported_id_field eikind) ->
+        find_in_module_with_includes Exported_id_field (
+            fun lid ->
+            let id = lid.ident in
+            find_in_record lid.ns id r k_record
+        ) Cont_ignore env (lid_of_ids curmod_ns) id
 
       | _ ->
         Cont_ignore
@@ -224,7 +307,7 @@ let try_lookup_id env (id:ident) =
   match unmangleOpName id with
   | Some f -> Some f
   | _ ->
-    try_lookup_id'' env id (fun r -> Cont_ok (found_local_binding r)) (fun _ -> Cont_fail) (fun _ -> Cont_ignore) (fun i -> find_in_module env i (fun _ _ -> Cont_fail) Cont_ignore) (fun _ _ -> Cont_fail)
+    try_lookup_id'' env id Exported_id_term_type (fun r -> Cont_ok (found_local_binding r)) (fun _ -> Cont_fail) (fun _ -> Cont_ignore) (fun i -> find_in_module env i (fun _ _ -> Cont_fail) Cont_ignore) (fun _ _ -> Cont_fail)
 
 (* Unqualified identifier lookup, if lookup in all open namespaces failed. *)
 
@@ -285,10 +368,11 @@ let resolve_module_name env lid (honor_ns: bool) : option<lident> =
 let resolve_in_open_namespaces''
   env
   lid
+  (eikind: exported_id_kind)
   (k_local_binding: local_binding -> cont_t<'a>)
   (k_rec_binding:   rec_binding   -> cont_t<'a>)
   (k_record: (record_or_dc * fieldname) -> cont_t<'a>)
-  (f_module: cont_t<'a> -> lident -> cont_t<'a>)
+  (f_module: lident -> cont_t<'a>)
   (l_default: cont_t<'a> -> ident -> cont_t<'a>)
   : option<'a> =
   match lid.ns with
@@ -296,11 +380,10 @@ let resolve_in_open_namespaces''
     begin match resolve_module_name env (set_lid_range (lid_of_ids lid.ns) (range_of_lid lid)) true with
     | None -> None
     | Some modul ->
-        let lid' = qual modul lid.ident in
-        option_of_cont (fun _ -> None) (f_module Cont_fail lid')
+        option_of_cont (fun _ -> None) (find_in_module_with_includes eikind f_module Cont_fail env modul lid.ident)
     end
   | [] ->
-    try_lookup_id'' env lid.ident k_local_binding k_rec_binding k_record (f_module Cont_ignore) l_default
+    try_lookup_id'' env lid.ident eikind k_local_binding k_rec_binding k_record f_module l_default
 
 let cont_of_option (k_none: cont_t<'a>) = function
     | Some v -> Cont_ok v
@@ -314,9 +397,9 @@ let resolve_in_open_namespaces'
   (k_global_def: lident -> (sigelt * bool) -> option<'a>)
   : option<'a> =
   let k_global_def' k lid def = cont_of_option k (k_global_def lid def) in
-  let f_module k lid' = find_in_module env lid' (k_global_def' k) k in
+  let f_module lid' = let k = Cont_ignore in find_in_module env lid' (k_global_def' k) k in
   let l_default k i = lookup_default_id env i (k_global_def' k) k in
-  resolve_in_open_namespaces'' env lid (fun l -> cont_of_option Cont_fail (k_local_binding l)) (fun r -> cont_of_option Cont_fail (k_rec_binding r)) (fun _ -> Cont_ignore) f_module l_default
+  resolve_in_open_namespaces'' env lid Exported_id_term_type (fun l -> cont_of_option Cont_fail (k_local_binding l)) (fun r -> cont_of_option Cont_fail (k_rec_binding r)) (fun _ -> Cont_ignore) f_module l_default
 
 let fv_qual_of_se = function
     | Sig_datacon(_, _, _, l, _, quals, _, _) ->
@@ -515,12 +598,17 @@ let extract_record (e:env) (new_globs: ref<(list<scope_mod>)>) = function
         begin match must <| find_dc dc with
             | Sig_datacon(constrname, _, t, _, _, _, _, _) ->
                 let formals, _ = U.arrow_formals t in
-                let is_rec = is_rec tags in 
-                let fields = formals |> List.collect (fun (x,q) ->
+                let is_rec = is_rec tags in
+                let formals' = formals |> List.collect (fun (x,q) ->
                         if S.is_null_bv x
                         || (is_rec && S.is_implicit q)
                         then []
-                        else [(mk_field_projector_name_from_ident constrname (if is_rec then Util.unmangle_field_name x.ppname else x.ppname), x.sort)]) in
+                        else [(x,q)] )
+                in
+                let fields' = formals' |> List.map (fun (x,q) -> ((if is_rec then Util.unmangle_field_name x.ppname else x.ppname), x.sort))
+                in
+                let fields = fields' |> List.map (fun (xid,xsort) -> mk_field_projector_name_from_ident constrname xid, xsort)
+                in
                 let record = {typename=typename;
                               constrname=constrname;
                               parms=parms;
@@ -530,6 +618,22 @@ let extract_record (e:env) (new_globs: ref<(list<scope_mod>)>) = function
                 top-level definitions, to allow shadowing field names
                 that were reachable through previous "open"s. *)
                 let () = new_globs := Record_or_dc record :: !new_globs in
+                (* the field names are added into the set of exported fields for "include" *)
+                let () =
+                  let add_field (id, _) =
+                    let modul = (lid_of_ids constrname.ns).str in
+                    match get_exported_id_set e modul with
+                    | Some my_ex ->
+                      let my_exported_ids = my_ex Exported_id_field in
+                      let () = my_exported_ids := Util.set_add id.idText !my_exported_ids in
+                      (* also add the projector name *)
+                      let projname = (mk_field_projector_name_from_ident constrname id).ident.idText in
+                      let () = my_exported_ids := Util.set_add projname !my_exported_ids in
+                      ()
+                    | None -> () (* current module was not prepared? should not happen *)
+                  in
+                  List.iter add_field fields'
+                in
                 insert_record_cache record
             | _ -> ()
         end
@@ -545,7 +649,7 @@ let try_lookup_record_or_dc_by_field_name env (fieldname:lident) =
     Util.find_map (peek_record_cache()) (fun record ->
       option_of_cont (fun _ -> None) (find_in_record ns id record (fun r -> Cont_ok r))
     ) in
-  resolve_in_open_namespaces'' env fieldname (fun _ -> Cont_ignore) (fun _ -> Cont_ignore) (fun r -> Cont_ok r)  (fun k fn -> cont_of_option k (find_in_cache fn)) (fun k _ -> k)
+  resolve_in_open_namespaces'' env fieldname Exported_id_field (fun _ -> Cont_ignore) (fun _ -> Cont_ignore) (fun r -> Cont_ok r)  (fun fn -> cont_of_option Cont_ignore (find_in_cache fn)) (fun k _ -> k)
 
 let try_lookup_record_by_field_name env (fieldname:lident) =
     match try_lookup_record_or_dc_by_field_name env fieldname with 
@@ -566,11 +670,28 @@ let qualify_field_to_record env (recd:record_or_dc) (f:lident) =
       if lid_equals fname f
       then Some(fname)
       else None) in
-  resolve_in_open_namespaces'' env f (fun _ -> Cont_ignore) (fun _ -> Cont_ignore) (fun r -> Cont_ok (snd r)) (fun k fn -> cont_of_option k (qualify fn)) (fun k _ -> k)
+  resolve_in_open_namespaces'' env f Exported_id_field (fun _ -> Cont_ignore) (fun _ -> Cont_ignore) (fun r -> Cont_ok (snd r)) (fun  fn -> cont_of_option Cont_ignore (qualify fn)) (fun k _ -> k)
+
+let string_set_ref_new () = Util.mk_ref (Util.new_set Util.compare Util.hashcode)
+let exported_id_set_new () =
+    let term_type_set = string_set_ref_new () in
+    let field_set = string_set_ref_new () in
+    function
+    | Exported_id_term_type -> term_type_set
+    | Exported_id_field -> field_set
+
+let empty_include_smap : Util.smap<(ref<(list<lident>)>)> = new_sigmap()
+let empty_exported_id_smap : Util.smap<exported_id_set> = new_sigmap()
 
 let unique any_val exclude_if env lid =
-  let this_env = {env with scope_mods=[]} in
-  match try_lookup_lid' any_val exclude_if env lid with
+  (* Disable name resolution altogether, thus lid is assumed to be fully qualified *)
+  let filter_scope_mods = function
+    | Rec_binding _
+        -> true
+    | _ -> false
+  in
+  let this_env = {env with scope_mods = List.filter filter_scope_mods env.scope_mods; exported_ids=empty_exported_id_smap; includes=empty_include_smap } in
+  match try_lookup_lid' any_val exclude_if this_env lid with
     | None -> true
     | Some _ -> false
 
@@ -625,6 +746,15 @@ let push_sigelt env s =
       declarations, to allow shadowing of definitions that were
       formerly reachable by previous "open"s. *)
       let () = globals := Top_level_def lid.ident :: !globals in
+      (* the identifier is added into the list of global identifiers
+         of the corresponding module to shadow any "include" *)
+      let modul = (lid_of_ids lid.ns).str in
+      let () = match get_exported_id_set env modul with
+      | Some f ->
+        let my_exported_ids = f Exported_id_term_type in
+        my_exported_ids := Util.set_add lid.ident.idText !my_exported_ids
+      | None -> () (* current module was not prepared? should not happen *)
+      in
       Util.smap_add (sigmap env) lid.str (se, env.iface && not env.admitted_iface)));
   let env = {env with scope_mods = !globals } in
   env
@@ -643,6 +773,44 @@ let push_namespace env ns =
   in
      push_scope_mod env (Open_module_or_namespace (ns', kd))
 
+let push_include env ns =
+    (* similarly to push_namespace in the case of modules, we allow
+       module abbrevs, but not namespace resolution *)
+    match resolve_module_name env ns false with
+    | Some ns ->
+      (* from within the current module, include is equivalent to open *)
+      let env = push_scope_mod env (Open_module_or_namespace (ns, Open_module)) in
+      (* update the list of includes *)
+      let curmod = (current_module env).str in
+      let () = match Util.smap_try_find env.includes curmod with
+      | None -> ()
+      | Some incl -> incl := ns :: !incl
+      in
+      (* the names of the included module and its transitively
+         included modules shadow the names of the current module *)
+      begin match get_trans_exported_id_set env ns.str with
+      | Some ns_trans_exports ->
+        let () = match (get_exported_id_set env curmod, get_trans_exported_id_set env curmod) with
+        | (Some cur_exports, Some cur_trans_exports) ->
+          let update_exports (k: exported_id_kind) =
+            let ns_ex = ! (ns_trans_exports k) in
+            let ex = cur_exports k in
+            let () = ex := Util.set_difference (!ex) ns_ex in
+            let trans_ex = cur_trans_exports k in
+            let () = trans_ex := Util.set_union (!ex) ns_ex in
+            ()
+          in
+          List.iter update_exports all_exported_id_kinds
+        | _ -> () (* current module was not prepared? should not happen *)
+        in
+        env
+      | None ->
+        (* module to be included was not prepared, so forbid the 'include'. It may be the case for modules such as FStar.ST, etc. *)
+        raise (Error (Util.format1 "include: Module %s was not prepared" ns.str, Ident.range_of_lid ns))
+      end
+    | _ ->
+      raise (Error (Util.format1 "include: Module %s cannot be found" ns.str, Ident.range_of_lid ns))
+
 let push_module_abbrev env x l =
   (* both namespace resolution and module abbrevs disabled:
      in 'module A = B', B must be fully qualified *)
@@ -688,6 +856,19 @@ let finish env modul =
            Util.smap_add (sigmap env) lid.str (decl, false))
 
     | _ -> ());
+  (* update the sets of transitively exported names of this module by
+     adding the unshadowed names defined only in the current module. *)
+  let curmod = (current_module env).str in
+  let () = match (get_exported_id_set env curmod, get_trans_exported_id_set env curmod) with
+    | (Some cur_ex, Some cur_trans_ex) ->
+      let update_exports eikind =
+        let cur_ex_set = ! (cur_ex eikind) in
+        let cur_trans_ex_set_ref = cur_trans_ex eikind in
+        cur_trans_ex_set_ref := Util.set_union cur_ex_set (!cur_trans_ex_set_ref)
+       in
+       List.iter update_exports all_exported_id_kinds
+    | _ -> ()
+  in
   {env with
     curmodule=None;
     modules=(modul.name, modul)::env.modules;
@@ -776,6 +957,12 @@ let prepare_module_or_interface intf admitted env mname =
       then let ns = Ident.lid_of_ids mname.ns in
            ns::open_ns //the namespace of the current module, if any, is implicitly in scope
       else open_ns in
+    (* Create new empty set of exported identifiers for the current module, for 'include' *)
+    let () = Util.smap_add env.exported_ids mname.str (exported_id_set_new ()) in
+    (* Create new empty set of transitively exported identifiers for the current module, for 'include' *)
+    let () = Util.smap_add env.trans_exported_ids mname.str (exported_id_set_new ()) in
+    (* Create new empty list of includes for the current module *)
+    let () = Util.smap_add env.includes mname.str (Util.mk_ref []) in
     {
       env with curmodule=Some mname;
       sigmap=env.sigmap;
diff --git a/src/parser/env.fsi b/src/parser/env.fsi
index 95b284a6797..6f82ea8b7ac 100644
--- a/src/parser/env.fsi
+++ b/src/parser/env.fsi
@@ -57,11 +57,33 @@ type scope_mod =
 | Top_level_def            of ident           (* top-level definition for an unqualified identifier x to be resolved as curmodule.x. *)
 | Record_or_dc             of record_or_dc    (* to honor interleavings of "open" and record definitions *)
 
+type string_set = set<string>
+
+type exported_id_kind = (* kinds of identifiers exported by a module *)
+| Exported_id_term_type (* term and type identifiers *)
+| Exported_id_field     (* field identifiers *)
+type exported_id_set = exported_id_kind -> ref<string_set>
+
 type env = {
   curmodule:            option<lident>;                   (* name of the module being desugared *)
   curmonad:             option<ident>;                    (* current monad being desugared *)
   modules:              list<(lident * modul)>;           (* previously desugared modules *)
   scope_mods:           list<scope_mod>;                  (* toplevel or definition-local scope modifiers *)
+  exported_ids:         Util.smap<exported_id_set>;       (* identifiers (stored as strings for efficiency)
+                                                             reachable in a module, not shadowed by "include"
+                                                             declarations. Used only to handle such shadowings,
+                                                             not "private"/"abstract" definitions which it is
+                                                             enough to just remove from the sigmap. Formally,
+                                                             iden is in exported_ids[ModulA] if, and only if,
+                                                             there is no 'include ModulB' (with ModulB.iden
+                                                             defined or reachable) after iden in ModulA.
+                                                           *)  
+  trans_exported_ids:   Util.smap<exported_id_set>;       (* transitive version of exported_ids along the
+                                                             "include" relation, for each module: an identifier is in this set
+                                                             for a module if and only if it is defined either
+                                                             in this module or in one of its included modules.
+                                                           *)
+  includes:             Util.smap<(ref<(list<lident>)>)>; (* list of "includes" declarations for each module. *)
   sigaccum:             sigelts;                          (* type declarations being accumulated for the current module *)
   sigmap:               Util.smap<(sigelt * bool)>;       (* bool indicates that this was declared in an interface file *)
   default_result_effect:lident;                           (* either Tot or ML, depending on the what kind of term we're desugaring *)
@@ -102,6 +124,7 @@ val push_bv_mutable: env -> ident -> env * bv
 val push_top_level_rec_binding: env -> ident -> S.delta_depth -> env
 val push_sigelt: env -> sigelt -> env
 val push_namespace: env -> lident -> env
+val push_include: env -> lident -> env
 val push_module_abbrev : env -> ident -> lident -> env
 
 val pop: env -> env
diff --git a/src/parser/lexhelp.fs b/src/parser/lexhelp.fs
index 4d02716aabf..d2f937628ec 100644
--- a/src/parser/lexhelp.fs
+++ b/src/parser/lexhelp.fs
@@ -156,6 +156,7 @@ let keywords =
     ALWAYS, "if"         ,IF;
     ALWAYS, "kind"       ,KIND;
     ALWAYS, "in"         ,IN;
+    ALWAYS, "include"    ,INCLUDE;
     ALWAYS, "inline"     ,INLINE;
     ALWAYS, "inline_for_extraction"     ,INLINE_FOR_EXTRACTION;
     ALWAYS, "irreducible",IRREDUCIBLE;
diff --git a/src/parser/ml/lex.mll b/src/parser/ml/lex.mll
index 62ac618cc98..9f65d716ad5 100644
--- a/src/parser/ml/lex.mll
+++ b/src/parser/ml/lex.mll
@@ -58,6 +58,7 @@
     Hashtbl.add keywords "if"            IF          ;
     Hashtbl.add keywords "kind"          KIND        ;
     Hashtbl.add keywords "in"            IN          ;
+    Hashtbl.add keywords "include"       INCLUDE     ;
     Hashtbl.add keywords "inline"        INLINE      ;
     Hashtbl.add keywords "inline_for_extraction"        INLINE_FOR_EXTRACTION      ;
     Hashtbl.add keywords "irreducible"   IRREDUCIBLE ;
diff --git a/src/parser/ml/parse.mly b/src/parser/ml/parse.mly
index 25d4676b80e..4a3189cb586 100644
--- a/src/parser/ml/parse.mly
+++ b/src/parser/ml/parse.mly
@@ -147,6 +147,7 @@ let compile_op arity s =
 %token IFF
 %token IMPLIES
 %token IN
+%token INCLUDE
 %token INLINE
 %token INLINE_FOR_EXTRACTION
 %token <string * bool> INT
@@ -722,6 +723,9 @@ decl2:
   OPEN quident
     {let (_1, uid) = ((), $2) in
       ( Open uid )}
+| INCLUDE quident
+    {let (_1, uid) = ((), $2) in
+      ( Include uid )}
 | MODULE uident EQUALS quident
     {let (_1, uid1, _3, uid2) = ((), $2, (), $4) in
       (  ModuleAbbrev(uid1, uid2) )}
diff --git a/src/parser/parse.fsi b/src/parser/parse.fsi
index c4bef836bb6..b42197f21ee 100644
--- a/src/parser/parse.fsi
+++ b/src/parser/parse.fsi
@@ -90,6 +90,7 @@ type token =
   | INT of (string * bool)
   | INLINE_FOR_EXTRACTION
   | INLINE
+  | INCLUDE
   | IN
   | IMPLIES
   | IFF
@@ -224,6 +225,7 @@ type tokenId =
     | TOKEN_INT
     | TOKEN_INLINE_FOR_EXTRACTION
     | TOKEN_INLINE
+    | TOKEN_INCLUDE
     | TOKEN_IN
     | TOKEN_IMPLIES
     | TOKEN_IFF
diff --git a/src/parser/parse.fsy b/src/parser/parse.fsy
index 102d008fe85..ce51986664f 100644
--- a/src/parser/parse.fsy
+++ b/src/parser/parse.fsy
@@ -149,6 +149,7 @@ let compile_op arity s =
 %token IFF
 %token IMPLIES
 %token IN
+%token INCLUDE
 %token INLINE
 %token INLINE_FOR_EXTRACTION
 %token <string * bool> INT
@@ -724,6 +725,9 @@ decl2:
   OPEN quident
     {let (_1, uid) = ((), $2) in
       ( Open uid )}
+| INCLUDE quident
+    {let (_1, uid) = ((), $2) in
+      ( Include uid )}
 | MODULE uident EQUALS quident
     {let (_1, uid1, _3, uid2) = ((), $2, (), $4) in
       (  ModuleAbbrev(uid1, uid2) )}
diff --git a/src/parser/parse.mly b/src/parser/parse.mly
index 9954b78f8f7..e1a829160ba 100644
--- a/src/parser/parse.mly
+++ b/src/parser/parse.mly
@@ -134,6 +134,7 @@ let compile_op arity s =
 %token EXCEPTION FALSE L_FALSE FUN FUNCTION IF IN MODULE DEFAULT
 %token MATCH OF
 %token OPEN REC MUTABLE THEN TRUE L_TRUE TRY TYPE EFFECT VAL
+%token INCLUDE
 %token WHEN WITH HASH AMP LPAREN RPAREN LPAREN_RPAREN COMMA LARROW RARROW
 %token IFF IMPLIES CONJUNCTION DISJUNCTION
 %token DOT COLON COLON_COLON SEMICOLON
@@ -223,6 +224,8 @@ decl:
 decl2:
   | OPEN uid=quident
       { Open uid }
+  | INCLUDE uid=quident
+      { Include uid }
   | MODULE uid1=uident EQUALS uid2=quident
       {  ModuleAbbrev(uid1, uid2) }
   | MODULE uid=quident
diff --git a/src/parser/tosyntax.fs b/src/parser/tosyntax.fs
index ddfb9490052..fd49474530b 100644
--- a/src/parser/tosyntax.fs
+++ b/src/parser/tosyntax.fs
@@ -1641,6 +1641,10 @@ and desugar_decl env (d:decl) : (env_t * sigelts) =
     let env = Env.push_namespace env lid in
     env, []
 
+  | Include lid ->
+    let env = Env.push_include env lid in
+    env, []
+
   | ModuleAbbrev(x, l) ->
     Env.push_module_abbrev env x l, []