anchor.diff:  
   let has_prims_cache (l: list<string>) :bool = List.mem "Prims.cache" l
   
  +
   open FStar.TypeChecker.Env
   let u_parse env fn =
  -    try
  -        match Parser.ParseIt.parse (Inl fn) with
  -            | Inl (Inl ast) ->
  -                Parser.ToSyntax.desugar_file env ast
  -
  -            | Inl (Inr _) ->
  -                Util.print1_error "%s expected a module\n" fn;
  -                exit 1
  -
  -            | Inr (msg, r) ->
  -                Util.print_string <| Print.format_error r msg;
  -                exit 1
  +  try
  +    match Parser.ParseIt.parse (Inl fn) with
  +    | Inl (Inl ast) ->
  +        Parser.ToSyntax.desugar_file env ast
  +    | Inl (Inr _) ->
  +        Util.print1_error "%s expected a module\n" fn;
  +        exit 1
  +    | Inr (msg, r) ->
  +        Util.print_string <| Print.format_error r msg;
  +        exit 1
       with e when (!Options.trace_error
  -                    && FStar.Syntax.Util.handleable e
  -                    && (FStar.Syntax.Util.handle_err false () e; false)) ->
  -                    failwith "Impossible"
  -
  +                && FStar.Syntax.Util.handleable e
  +                && (FStar.Syntax.Util.handle_err false () e; false)) ->
  +                failwith "Impossible"
           | e when (not !Options.trace_error && FStar.Syntax.Util.handleable e) ->
  -        FStar.Syntax.Util.handle_err false () e;
  -        exit 1
  +            FStar.Syntax.Util.handle_err false () e;
  +            exit 1
   
   let u_tc_prims () =
  -    let solver = if !Options.verify then SMTEncoding.Encode.solver else SMTEncoding.Encode.dummy in
  -    let env = FStar.TypeChecker.Env.initial_env
  -         FStar.TypeChecker.Tc.type_of
  -         solver
  -         Const.prims_lid in
  -    env.solver.init env;
  -    let p = Options.prims () in
  -    let dsenv, prims_mod = u_parse (Parser.Env.empty_env()) p in
  -    let prims_mod, env = FStar.TypeChecker.Tc.check_module env (List.hd prims_mod) in
  -    prims_mod, dsenv, env
  -
  +  let solver = if !Options.verify then SMTEncoding.Encode.solver else SMTEncoding.Encode.dummy in
  +  let env = FStar.TypeChecker.Env.initial_env
  +            FStar.TypeChecker.Tc.type_of
  +            solver
  +            Const.prims_lid in
  +  env.solver.init env;
  +  let p = Options.prims () in
  +  let dsenv, prims_mod = u_parse (Parser.Env.empty_env()) p in
  +  let prims_mod, env = FStar.TypeChecker.Tc.check_module env (List.hd prims_mod) in
  +  prims_mod, dsenv, env
   
   let test_universes filenames =
  -    try
  -        let prims_mod, dsenv, env = u_tc_prims() in
  -        let dsenv, mods, env = List.fold_left (fun (dsenv, fmods, env) fn ->
  -           Util.print1 "Parsing file %s\n" fn;
  -           let dsenv, mods = u_parse dsenv fn in
  -           let _, env = TypeChecker.Tc.check_module env (List.hd mods) in
  -           dsenv, mods@fmods, env) (dsenv, [], env) filenames in
  -        env.solver.finish();
  -        dsenv, mods, env
  -    with
  -        | Syntax.Syntax.Error(msg, r) when not (!Options.trace_error) ->
  -          Util.print_error (Util.format2 "%s\n%s\n" (Range.string_of_range r) msg);
  -          exit 1
  +  try
  +    let prims_mod, dsenv, env = u_tc_prims() in
  +    let dsenv, mods, env =
  +      List.fold_left (fun (dsenv, fmods, env) fn ->
  +                     Util.print1 "Parsing file %s\n" fn;
  +                     let dsenv, mods = u_parse dsenv fn in
  +                     let _, env = TypeChecker.Tc.check_module env (List.hd mods) in
  +                     dsenv, mods@fmods, env) (dsenv, [], env) filenames in
  +    env.solver.finish();
  +    dsenv, mods, env
  +  with
  +  | Syntax.Syntax.Error(msg, r) when not (!Options.trace_error) ->
  +      Util.print_error (Util.format2 "%s\n%s\n" (Range.string_of_range r) msg);
  +      exit 1
   
   open FStar.Tc.Env
   let tc_prims () =
  -    let solver = if !Options.verify then ToSMT.Encode.solver else ToSMT.Encode.dummy in
  -    let env = Tc.Env.initial_env solver Const.prims_lid in
  -    env.solver.init env;
  -
  -    let p = Options.prims () in
  -    let dsenv, prims_mod = Parser.Driver.parse_file (Parser.DesugarEnv.empty_env()) p in
  -    let prims_mod, env = Tc.Tc.check_module env (List.hd prims_mod) in
  -    prims_mod, dsenv, env
  +  let solver = if !Options.verify then ToSMT.Encode.solver else ToSMT.Encode.dummy in
  +  let env = Tc.Env.initial_env solver Const.prims_lid in
  +  env.solver.init env;
  +
  +  let p = Options.prims () in
  +  let dsenv, prims_mod = Parser.Driver.parse_file (Parser.DesugarEnv.empty_env()) p in
  +  let prims_mod, env = Tc.Tc.check_module env (List.hd prims_mod) in
  +  prims_mod, dsenv, env
   
   let report_errors nopt =
  -    let errs = match nopt with
  -        | None -> Tc.Errors.get_err_count ()
  -        | Some n -> n in
  -    if errs>0
  -    then begin
  -        Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
  -        exit 1
  -    end
  +  let errs =
  +    match nopt with
  +    | None -> Tc.Errors.get_err_count ()
  +    | Some n -> n in
  +  if errs > 0 then begin
  +    Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
  +    exit 1
  +  end
   
   let report_universes_errors nopt =
  -    let errs = match nopt with
  -        | None -> TypeChecker.Errors.get_err_count ()
  -        | Some n -> n in
  -    if errs>0
  -    then begin
  -        Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
  -        exit 1
  -    end
  +  let errs =
  +    match nopt with
  +    | None -> TypeChecker.Errors.get_err_count ()
  +    | Some n -> n in
  +  if errs > 0 then begin
  +    Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
  +    exit 1
  +  end
   
   let tc_one_file dsenv env fn =
  -    let dsenv, fmods = Parser.Driver.parse_file dsenv fn in
  -    let env, all_mods = fmods |> List.fold_left (fun (env, all_mods) m ->
  -        let ms, env = Tc.Tc.check_module env m in
  -        env, ms@all_mods) (env, []) in
  -    dsenv, env, List.rev all_mods
  +  let dsenv, fmods = Parser.Driver.parse_file dsenv fn in
  +  let env, all_mods =
  +    fmods |> List.fold_left (fun (env, all_mods) m ->
  +                            let ms, env = Tc.Tc.check_module env m in
  +                            env, ms@all_mods) (env, []) in
  +  dsenv, env, List.rev all_mods
   
   let tc_one_fragment curmod dsenv env frag =
  -    try
  -        match Parser.Driver.parse_fragment curmod dsenv frag with
  -            | Parser.Driver.Empty ->
  -              Some (curmod, dsenv, env)
  -
  -            | Parser.Driver.Modul (dsenv, modul) ->
  -              let env = match curmod with
  -                | None -> env
  -                | Some _ ->
  -                  raise (Absyn.Syntax.Err("Interactive mode only supports a single module at the top-level")) in
  -              let modul, env = Tc.Tc.tc_partial_modul env modul in
  -              Some (Some modul, dsenv, env)
  -
  -            | Parser.Driver.Decls (dsenv, decls) ->
  -              begin match curmod with
  -                | None -> Util.print_error "fragment without an enclosing module"; exit 1
  -                | Some modul ->
  -                  let modul, env  = Tc.Tc.tc_more_partial_modul env modul decls in
  -                  Some (Some modul, dsenv, env)
  -              end
  +  try
  +    match Parser.Driver.parse_fragment curmod dsenv frag with
  +    | Parser.Driver.Empty ->
  +        Some (curmod, dsenv, env)
  +    | Parser.Driver.Modul (dsenv, modul) ->
  +        let env =
  +          match curmod with
  +          | None -> env
  +          | Some _ -> raise (Absyn.Syntax.Err("Interactive mode only supports a single module at the top-level")) in
  +        let modul, env = Tc.Tc.tc_partial_modul env modul in
  +        Some (Some modul, dsenv, env)
  +    | Parser.Driver.Decls (dsenv, decls) -> begin
  +        match curmod with
  +        | None -> Util.print_error "fragment without an enclosing module"; exit 1
  +        | Some modul ->
  +            let modul, env  = Tc.Tc.tc_more_partial_modul env modul decls in
  +            Some (Some modul, dsenv, env) end
       with
  -        | Absyn.Syntax.Error(msg, r) ->
  +      | Absyn.Syntax.Error(msg, r) ->
             Tc.Errors.add_errors env [(msg,r)];
             None
  -
  -        | Absyn.Syntax.Err msg ->
  +      | Absyn.Syntax.Err msg ->
             Tc.Errors.add_errors env [(msg,Absyn.Syntax.dummyRange)];
             None
  -
  -        | e -> raise e
  +      | e -> raise e
   
   type input_chunks =
  -    | Push of string
  -    | Pop  of string
  -    | Code of string * (string * string)
  -
  -type stack_elt =
  -    (option<modul>
  -     * Parser.DesugarEnv.env
  -     * Tc.Env.env)
  +  | Push of string
  +  | Pop  of string
  +  | Code of string * (string * string)
  +
  +type stack_elt = (option<modul> * Parser.DesugarEnv.env * Tc.Env.env)
   type stack = list<stack_elt>
   
  -
   let batch_mode_tc_no_prims dsenv env filenames admit_fsi =
  -    let all_mods, dsenv, env = filenames |> List.fold_left (fun (all_mods, dsenv, env) f ->
  -        Util.reset_gensym();
  -        let dsenv, env, ms = tc_one_file dsenv env f in
  -        all_mods@ms, dsenv, env)
  -        ([], dsenv, env) in
  -
  -    if !Options.interactive && Tc.Errors.get_err_count () = 0
  -    then env.solver.refresh()
  -    else env.solver.finish();
  -    all_mods, dsenv, env
  +  let all_mods, dsenv, env =
  +    filenames |> List.fold_left (fun (all_mods, dsenv, env) f ->
  +                                Util.reset_gensym();
  +                                let dsenv, env, ms = tc_one_file dsenv env f in
  +                                all_mods@ms, dsenv, env)
  +                                ([], dsenv, env) in
  +  if !Options.interactive && Tc.Errors.get_err_count () = 0
  +  then env.solver.refresh()
  +  else env.solver.finish();
  +  all_mods, dsenv, env
   
   let find_deps_if_needed files =
  -    if !Options.explicit_deps then
  -      files, []
  -    else
  -      let _, deps = Parser.Dep.collect files in
  -      let deps = List.rev deps in
  -      let deps =
  -        if basename (List.hd deps) = "prims.fst" then
  -          List.tl deps
  -        else begin
  -          Util.print_error "dependency analysis did not find prims.fst?!";
  -          exit 1
  -        end
  -      in
  -      let admit_fsi = ref [] in
  -      List.iter (fun d ->
  -        let d = basename d in
  -        if get_file_extension d = "fsti" then
  -          admit_fsi := substring d 0 (String.length d - 5) :: !admit_fsi
  -        else if get_file_extension d = "fsi" then begin
  -          admit_fsi := substring d 0 (String.length d - 4) :: !admit_fsi
  -        end
  -      ) deps;
  -      deps, !admit_fsi
  +  if !Options.explicit_deps then
  +    files, []
  +  else
  +    let _, deps = Parser.Dep.collect files in
  +    let deps = List.rev deps in
  +    let deps =
  +      if basename (List.hd deps) = "prims.fst" then
  +        List.tl deps
  +      else begin
  +        Util.print_error "dependency analysis did not find prims.fst?!";
  +        exit 1
  +      end
  +    in
  +    let admit_fsi = ref [] in
  +    List.iter (fun d ->
  +              let d = basename d in
  +              if get_file_extension d = "fsti" then
  +                admit_fsi := substring d 0 (String.length d - 5) :: !admit_fsi
  +              else if get_file_extension d = "fsi" then begin
  +                admit_fsi := substring d 0 (String.length d - 4) :: !admit_fsi end
  +    ) deps;
  +    deps, !admit_fsi
   
   let batch_mode_tc filenames =
  -    let prims_mod, dsenv, env = tc_prims () in
  -
  -    let filenames, admit_fsi = find_deps_if_needed filenames in
  -    let all_mods, dsenv, env = batch_mode_tc_no_prims dsenv env filenames admit_fsi in
  -    prims_mod @ all_mods, dsenv, env
  +  let prims_mod, dsenv, env = tc_prims () in
  +  let filenames, admit_fsi = find_deps_if_needed filenames in
  +  let all_mods, dsenv, env = batch_mode_tc_no_prims dsenv env filenames admit_fsi in
  +  prims_mod @ all_mods, dsenv, env
   
   let finished_message fmods =
  -    if not !Options.silent
  -    then begin
  -        let msg =
  -            if !Options.verify then "Verifying"
  -            else if !Options.pretype then "Lax type-checked"
  -            else "Parsed and desugared" in
  -         fmods |> List.iter (fun m ->
  -            let tag = if m.is_interface then "i'face" else "module" in
  -            if Options.should_print_message m.name.str
  -            then Util.print_string (Util.format3 "%s %s: %s\n" msg tag (Syntax.text_of_lid m.name)));
  -         print_string (Util.format1 "%s\n" (Util.colorize_bold "All verification conditions discharged successfully"))
  +  if not !Options.silent then begin
  +    let msg =
  +      if !Options.verify then "Verifying"
  +      else if !Options.pretype then "Lax type-checked"
  +      else "Parsed and desugared" in
  +        fmods |> List.iter (fun m ->
  +                 let tag = if m.is_interface then "i'face" else "module" in
  +                 if Options.should_print_message m.name.str
  +                 then Util.print_string (Util.format3 "%s %s: %s\n" msg tag (Syntax.text_of_lid m.name)));
  +        print_string (Util.format1 "%s\n" (Util.colorize_bold "All verification conditions discharged successfully"))
       end
   
   type interactive_state = {
  
positive.code:   s.buffer := !s.buffer @ [ read_chunk () ]
  
  let interactive_mode dsenv env =
      if Option.isSome !Options.codegen
      then (Util.print_warning "code-generation is not supported in interactive mode, ignoring the codegen flag");
  
      let rec go (stack:stack) (curmod:option<modul>) dsenv env =
          begin match shift_chunk () with
              | Pop msg ->
                Parser.DesugarEnv.pop dsenv |> ignore;
                Tc.Env.pop env msg |> ignore;
                env.solver.refresh();
                Options.reset_options() |> ignore;
                let (curmod, dsenv, env), stack = match stack with
                  | [] -> Util.print_error "too many pops"; exit 1
                  | hd::tl -> hd, tl in
                go stack curmod dsenv env
  
              | Push msg ->
                let stack = (curmod, dsenv, env)::stack in
                let dsenv = Parser.DesugarEnv.push dsenv in
                let env = Tc.Env.push env msg in
                go stack curmod dsenv env
  
              | Code (text, (ok, fail)) ->
                  let mark dsenv env =
                      let dsenv = Parser.DesugarEnv.mark dsenv in
                      let env = Tc.Env.mark env in
                      dsenv, env in
  
                  let reset_mark dsenv env =
                      let dsenv = Parser.DesugarEnv.reset_mark dsenv in
                      let env = Tc.Env.reset_mark env in
                      dsenv, env in
  
                  let commit_mark dsenv env =
                      let dsenv = Parser.DesugarEnv.commit_mark dsenv in
                      let env = Tc.Env.commit_mark env in
                      dsenv, env in
  
                  let fail curmod dsenv_mark env_mark =
                      Tc.Errors.report_all() |> ignore;
                      Tc.Errors.num_errs := 0;
                      Util.print1 "%s\n" fail;
                      let dsenv, env = reset_mark dsenv_mark env_mark in
                      go stack curmod dsenv env in
  
                let dsenv_mark, env_mark = mark dsenv env in
                let res = tc_one_fragment curmod dsenv_mark env_mark text in
  
                begin match res with
                  | Some (curmod, dsenv, env) ->
                    if !Tc.Errors.num_errs=0
                    then begin
                       Util.print1 "\n%s\n" ok;
                       let dsenv, env = commit_mark dsenv env in
                       go stack curmod dsenv env
                    end
                    else fail curmod dsenv_mark env_mark
  
                  | _ ->
                    fail curmod dsenv_mark env_mark
                end
          end in
  
      go [] None dsenv env
  
  
  let codegen fmods env=
      if !Options.codegen = Some "OCaml"
      || !Options.codegen = Some "FSharp"
      then begin
          let c, mllibs = Util.fold_map Extraction.ML.ExtractMod.extract (Extraction.ML.Env.mkContext env) fmods in
          let mllibs = List.flatten mllibs in
          let ext = if !Options.codegen = Some "FSharp" then ".fs" else ".ml" in
          let newDocs = List.collect Extraction.ML.Code.doc_of_mllib mllibs in
  //                           else List.collect Extraction.OCaml.Code.doc_of_mllib mllibs, ".ml" in
          List.iter (fun (n,d) -> Util.write_file (Options.prependOutputDir (n^ext)) (FStar.Format.pretty 120 d)) newDocs
      end
  
  exception Found of string
  
negative.code: open FStar.Tc.Util
  open FStar.Ident
  
  
  let process_args () =
    let file_list = Util.mk_ref [] in
    let res = Getopt.parse_cmdline (Options.specs()) (fun i -> file_list := !file_list @ [i]) in
  