anchor.diff:  (***********************************************************************)
   (* Interactive mode: checking a fragment of a code                     *)
   (***********************************************************************)
  +// FIXME is_interface_dependence is always false
   let tc_one_fragment curmod (env:TcEnv.env) (frag, is_interface_dependence) =
     match Parser.Driver.parse_fragment frag with
  -  | Parser.Driver.Empty ->
  +  | Parser.Driver.Empty
  +  | Parser.Driver.Decls [] ->
       (curmod, env)
   
     | Parser.Driver.Modul ast_modul ->
  
positive.code:     (Some modul, env)
  
    | Parser.Driver.Decls ast_decls ->
      let env, ast_decls_l =
            BU.fold_map
                (fun env a_decl ->
                    let decls, env =
  
negative.code:                   env, decls)
                env
                ast_decls in
        let sigelts, env = with_tcenv env <| Desugar.decls_to_sigelts (List.flatten ast_decls_l) in
        let modul, _, env  = if DsEnv.syntax_only env.dsenv then (modul, [], env)
                             else Tc.tc_more_partial_modul env modul sigelts in
        (Some modul, env)
  
  let load_interface_decls env interface_file_name : FStar.TypeChecker.Env.env =
    let r = FStar.Parser.ParseIt.parse (Inl interface_file_name) in
    match r with
    | Inl (Inl (FStar.Parser.AST.Interface(l, decls, _)), _) ->
      snd (with_tcenv env <| FStar.ToSyntax.Interleave.initialize_interface l decls)
    | Inl _ ->
      raise (FStar.Errors.Err(BU.format1 "Unexpected result from parsing %s; expected a single interface"
                               interface_file_name))
    | Inr (err, rng) ->
      raise (FStar.Errors.Error(err, rng))
  
  (***********************************************************************)
  (* Batch mode: checking a file                                         *)
  