anchor.diff:            then BU.format2 "let %s : %s" (Print.lbname_to_string lb.lbname) (Print.term_to_string (*env*) lb.lbtyp)
             else "") |> String.concat "\n");
   
  -    let env = Env.push_sigelt env se in
  -    [se], env, []
  +    [se], []
   
   
   let for_export hidden se : list<sigelt> * list<lident> =
  
positive.code:     *)
      let env = Env.set_range env r in
      let se = tc_lex_t env ses quals lids  in
      [se], Env.push_sigelt env se, []
  
    | Sig_bundle(ses, quals, lids, r) ->
      let env = Env.set_range env r in
      let ses,projectors_ses = tc_inductive env ses quals lids  in
      let env = List.fold_left (fun env' se -> Env.push_sigelt env' se) env ses in
      ses, env, projectors_ses
  
    | Sig_pragma(p, r) ->
      let set_options t s = match Options.set_options t s with
  
negative.code:             uvs, SS.close_univ_vars uvs t
      in
      let se = Sig_declare_typ(lid, uvs, t, quals, r) in
      [se], []
  
    | Sig_assume(lid, phi, quals, r) ->
      let se = tc_assume env lid phi quals r in
      [se], []
  
    | Sig_main(e, r) ->
      let env = Env.set_range env r in
  