anchor.diff:          | Attributes cattributes  ->
               List.iter collect_term cattributes
           | CalcProof (rel, init, steps) ->
  -            add_dep_on_module (Ident.lid_of_str "FStar.Calc");
  +            record.add_dep_on_module (Ident.lid_of_str "FStar.Calc") false;
               begin
               collect_term rel;
               collect_term init;
  
positive.code: open FStar.String
  open FStar.Ident
  open FStar.Errors
  open FStar.Parser
  
  module Const = FStar.Parser.Const
  
negative.code:     then [ UseImplementation mname ]
      else [] in
  
    let print_dependence_list deps =
      List.fold_left (fun s d -> s ^ "::" ^ dep_to_string d) "" deps in
  
    let data_from_cache = filename |> get_parsing_data_from_cache in
    if data_from_cache |> is_some then begin
      if Options.debug_any ()
      then
        BU.print1 "Reading parsing data for %s from its checked file\n" filename;
        data_from_cache |> must |> read_parsing_data_from_cache;
        BU.print1 "Dependences as read from the cache:%s\n" (print_dependence_list (record.get_deps ()));
        BU.print1 "Parsing data as read from the cache:%s\n" (str_of_parsing_data (data_from_cache |> must));
        data_from_cache |> must,
        record.get_deps (),
        record.get_inline_for_extraction (),
        mo_roots
    end
    else
        let num_of_toplevelmods = BU.mk_ref 0 in
  
        let auto_open = hard_coded_dependencies filename in
        List.iter record.record_open_module_or_namespace auto_open;
  
        let rec collect_module = function
          | Module (lid, decls)
          | Interface (lid, decls, _) ->
              check_module_declaration_against_filename lid filename;
              record.begin_module lid;
              collect_decls decls
  
        and collect_decls decls =
          List.iter (fun x -> collect_decl x.d;
                              List.iter collect_term x.attrs;
                              if List.contains Inline_for_extraction x.quals
                              then record.set_interface_inlining ()
                              ) decls
  
        and collect_decl d =
          match d with
          | Include lid
          | Open lid ->
              record.record_open false lid
          | Friend lid ->
              record.add_dep_on_module (lowercase_join_longident lid true |> Ident.lid_of_str) true
          | ModuleAbbrev (ident, lid) ->
              ignore (record.record_module_alias ident lid)
          | TopLevelLet (_, patterms) ->
              List.iter (fun (pat, t) -> collect_pattern pat; collect_term t) patterms
          | Main t
  