anchor.diff:    | None ->
       tc_decl' env se
   
  -let check_must_erase_attribute env se =
  -    match se.sigel with
  -    | Sig_let(lbs, l) ->
  -        if not (Options.ide())
  -        then
  -        begin
  -          match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
  -          | None ->
  -            ()
  -
  -          | Some iface_decls ->
  -            snd lbs |> List.iter (fun lb ->
  -                let lbname = BU.right lb.lbname in
  -                let has_iface_val =
  -                    iface_decls |> BU.for_some (FStar.Parser.AST.decl_is_val lbname.fv_name.v.ident)
  -                in
  -                if has_iface_val
  -                then
  -                    let must_erase =
  -                    TcUtil.must_erase_for_extraction env lb.lbdef in
  -                    let has_attr =
  -                    Env.fv_has_attr env
  -                                    lbname
  -                                    FStar.Parser.Const.must_erase_for_extraction_attr in
  -                    if must_erase && not has_attr
  -                    then
  -                        FStar.Errors.log_issue
  -                            (range_of_fv lbname)
  -                            (FStar.Errors.Error_MustEraseMissing,
  -                                BU.format2
  -                                    "Values of type `%s` will be erased during extraction, \
  -                                    but its interface hides this fact. Add the `must_erase_for_extraction` \
  -                                    attribute to the `val %s` declaration for this symbol in the interface"
  -                                    (Print.fv_to_string lbname)
  -                                    (Print.fv_to_string lbname)
  -                                    )
  -                    else if has_attr && not must_erase
  -                    then FStar.Errors.log_issue
  -                        (range_of_fv lbname)
  -                        (FStar.Errors.Error_MustEraseMissing,
  -                            BU.format1
  -                                "Values of type `%s` cannot be erased during extraction, \
  -                                but the `must_erase_for_extraction` attribute claims that it can. \
  -                                Please remove the attribute."
  -                                (Print.fv_to_string lbname)
  -                                ))
  -    end
  -
  -    | _ -> ()
  -
   let for_export env hidden se : list<sigelt> * list<lident> =
      (* Exporting symbols based on whether they have been marked 'abstract'
   
  
positive.code:     in
      aux l1 l2
  
  let tc_decl' env0 se: list<sigelt> * list<sigelt> * Env.env =
    let env = env0 in
    TcUtil.check_sigelt_quals env se;
  
negative.code:     List.iter (fun se -> env.solver.encode_sig env se) ses';
  
      let exports, hidden =
        if Options.use_extracted_interfaces () then List.rev_append ses' exports, []
        else
          let accum_exports_hidden (exports, hidden) se =
  