anchor.diff:      env
   
   let term_as_mlty g t0 =
  -    // if TcEnv.debug g.env_tcenv <| Options.Other "Extraction"
  -    // || TcEnv.debug g.env_tcenv <| Options.Other "ExtractNorm"
  -    // then
  -    BU.print1 "Starting to normalize type %s\n"
  +    if (TcEnv.debug g.env_tcenv <| Options.Other "Extraction"
  +        || TcEnv.debug g.env_tcenv <| Options.Other "ExtractNorm")
  +    && Options.use_nbe_for_extraction()
  +    then
  +      BU.print1 "Starting to normalize type %s\n"
                      (Print.term_to_string t0);
  -    let t = N.normalize extraction_norm_steps g.env_tcenv t0 in
  +    let t = N.normalize (get_extraction_norm_steps()) g.env_tcenv t0 in
       translate_term_to_mlty g t
   
   
  
positive.code:                         if Options.ml_ish()
                          then lb.lbdef
                          else let norm_call () =
                                   N.normalize (Env.PureSubtermsWithinComputations::extraction_norm_steps) tcenv lb.lbdef
                               in
                               if TcEnv.debug tcenv <| Options.Other "Extraction"
                               || TcEnv.debug tcenv <| Options.Other "ExtractNorm"
  
negative.code:      Env.Exclude Env.Zeta;
       Env.Primops;
       Env.Unascribe;
       Env.ForExtraction]
  
  let extraction_norm_steps_nbe =
    Env.NBE::extraction_norm_steps
  
  let get_extraction_norm_steps () = 
    if Options.use_nbe_for_extraction()
    then extraction_norm_steps_nbe
    else extraction_norm_steps
    
  let comp_no_args c =
      match c.n with
      | Total _
  