anchor.diff:    List.iter (fun fn -> discover_one (lowercase_module_name fn)) filenames;
   
     (* At this point, we have the (immediate) dependency graph of all the files. *)
  -  let immediate_graph = smap_copy dep_graph in
  -
  -  let topologically_sorted = BU.mk_ref [] in
  -
  -  (* Compute the transitive closure. *)
  -  let rec discover cycle key =
  -    let direct_deps, color = must (smap_try_find dep_graph key) in
  -    match color with
  -    | Gray ->
  -        Util.print1_warning "Recursive dependency on module %s\n" key;
  -        let cycle = cycle |> List.map file_names_of_key in
  -        Util.print1 "The cycle contains a subset of the modules in:\n%s \n" (String.concat "\n`used by` " cycle);
  -        print_graph immediate_graph;
  -        print_string "\n";
  -        exit 1
  -    | Black ->
  -        (* If the element has been visited already, then the map contains all its
  -         * dependencies. Otherwise, the map only contains its direct dependencies. *)
  -        ()
  -    | White ->
  -        (* Unvisited. Compute. *)
  -        smap_add dep_graph key (direct_deps, Gray);
  -        List.iter (fun k -> discover (k :: cycle) k) (dependences_of file_system_map dep_graph key);
  -        (* Mutate the graph (it now remembers transitive dependencies). *)
  -        smap_add dep_graph key (direct_deps, Black);
  -        (* Also build the topological sort (Tarjan's algorithm). *)
  -        topologically_sorted := key :: !topologically_sorted
  -  in
  -
  -  let discover k =
  -    topologically_sorted := [];
  -    discover [] k;
  -    !topologically_sorted
  +  (* Add additional edges between the filenames in the order in which they were provided *)
  +  let _ =
  +    List.fold_left
  +        (fun previous_file file ->
  +            add_dependence dep_graph file previous_file;
  +            file)
  +        (List.hd filenames)
  +        (List.tl filenames) in
  +
  +  let topological_module_dependences_of filename =
  +      let topologically_sorted = BU.mk_ref [] in
  +      (* Compute the transitive closure. *)
  +      let rec discover cycle filename =
  +        let direct_deps, color = must (smap_try_find dep_graph key) in
  +        match color with
  +        | Gray ->
  +            Util.print1_warning "Recursive dependency on module %s\n" key;
  +            let cycle = cycle |> List.map file_names_of_key in
  +            Util.print1 "The cycle contains a subset of the modules in:\n%s \n" (String.concat "\n`used by` " cycle);
  +            print_graph dep_graph;
  +            print_string "\n";
  +            exit 1
  +        | Black ->
  +            (* If the element has been visited already, then the map contains all its
  +             * dependencies. Otherwise, the map only contains its direct dependencies. *)
  +            ()
  +        | White ->
  +            (* Unvisited. Compute. *)
  +            smap_add dep_graph key (direct_deps, Gray);
  +            List.iter (fun k -> discover (k :: cycle) k) (dependences_of file_system_map dep_graph key);
  +            (* Mutate the graph (it now remembers transitive dependencies). *)
  +            smap_add dep_graph key (direct_deps, Black);
  +            (* Also build the topological sort (Tarjan's algorithm). *)
  +            topologically_sorted := key :: !topologically_sorted
  +      in
  +      discover [] filename;
  +      !topologically_sorted
     in
   
     let must_find k =
  
positive.code:         check_module_declaration_against_filename lid filename;
          if List.length lid.ns > 0 then
            ignore (enter_namespace original_map working_map (namespace_of_lid lid));
          (* We discovered a new file in the graph. *)
          begin match verify_mode with
          | VerifyAll ->
              (* Every module we discover is a module we verify. *)
              Options.add_verify_module (string_of_lid lid true)
          | VerifyFigureItOut ->
              (* Well... to put all the code in one place, the function takes an
               * argument that tells whether this is a root of the discovery (i.e.
               * we started from a file that was provided on the command-line. *)
              if is_user_provided_filename then
                Options.add_verify_module (string_of_lid lid true)
          | VerifyUserList ->
              (* Mutate the reference to acknowledge that we have found the file
               * the user mentioned in the first place (the code will later bail
               * if there a user-provided --verify_module argument referes to a
               * module that hasn't been found in the graph). *)
              List.iter (fun (m, r) ->
                if String.lowercase m = String.lowercase (string_of_lid lid true) then
                  r := true
              ) verify_flags
          end;
          collect_decls decls
  
    and collect_decls decls =
  
negative.code:     | [] -> ()
      | _ ->
        let module_name = Ident.lid_of_ids lid.ns in
        if add_dependence_edge module_name
        then ()
        else if Options.debug_any () then
              FStar.Errors.warn (range_of_lid lid)
                  (BU.format1 "Unbound module reference %s"
                                  (Ident.string_of_lid module_name))
  