anchor.diff:  
       let is_noeq = List.existsb (fun q -> q = Noeq) quals in
   
  -    if ((List.length tcs = 0) || ((lid_equals env.curmodule Const.prims_lid) && skip_prims_type ()) || is_noeq)
  -    then [sig_bndle], data_ops_ses
  -    else
  -        let is_unopteq = List.existsb (fun q -> q = Unopteq) quals in
  -        let ses =
  -          if is_unopteq then TcInductive.unoptimized_haseq_scheme sig_bndle tcs datas env0 tc_assume
  -          else TcInductive.optimized_haseq_scheme sig_bndle tcs datas env0 tc_assume
  -        in
  -        { sigel = Sig_bundle(tcs@datas, lids);
  -          sigquals = quals;
  -          sigrng = Env.get_range env0;
  -          sigmeta = default_sigmeta  }::ses, data_ops_ses
  +    let res =
  +        if ((List.length tcs = 0) || ((lid_equals env.curmodule Const.prims_lid) && skip_prims_type ()) || is_noeq)
  +        then [sig_bndle], data_ops_ses
  +        else
  +            let is_unopteq = List.existsb (fun q -> q = Unopteq) quals in
  +            let ses =
  +              if is_unopteq then TcInductive.unoptimized_haseq_scheme sig_bndle tcs datas env tc_assume
  +              else TcInductive.optimized_haseq_scheme sig_bndle tcs datas env tc_assume
  +            in
  +            { sigel = Sig_bundle(tcs@datas, lids);
  +              sigquals = quals;
  +              sigrng = Env.get_range env;
  +              sigmeta = default_sigmeta  }::ses, data_ops_ses in
  +    ignore (Env.pop env "tc_inductive");
  +    res
   
   
   (* [tc_decl env se] typechecks [se] in environment [env] and returns *)
   (* the list of typechecked sig_elts, and a list of new sig_elts elaborated during typechecking but not yet typechecked *)
  -and tc_decl env se: list<sigelt> * list<sigelt> =
  +let tc_decl env se: list<sigelt> * list<sigelt> =
     let env = set_hint_correlator env se in
     TcUtil.check_sigelt_quals env se;
     let r = se.sigrng in
  
positive.code:     //strict positivity check
      (if Options.no_positivity () || Options.lax ()  then ()  //skipping positivity check if lax mode
       else
         let env = push_sigelt env0 sig_bndle in
         let b = List.iter (fun ty ->
           let b = TcInductive.check_positivity ty env in
           if not b then
  
negative.code:     end
    | _ -> fail()
  
  let tc_eff_decl env0 (ed:Syntax.eff_decl) =
    assert (ed.univs = []); //no explicit universe variables in the source; Q: But what about re-type-checking a program?
    let effect_params_un, signature_un, opening = SS.open_term' ed.binders ed.signature in
    let effect_params, env, _ = tc_tparams env0 effect_params_un in
  