anchor.diff:      end;
       rebuild cfg env stack t
   
  -  | Steps (s, ps, dl) :: stack ->
  -    rebuild ({cfg with steps=s; primitive_steps=ps; delta_level=dl}) env stack t
  +  | Cfg cfg :: stack ->
  +    rebuild cfg env stack t
   
     | Meta(m, r)::stack ->
       let t = mk (Tm_meta(t, m)) r in
  
positive.code:                       end
                    end
  
                  | Steps (s, ps, dl) :: stack ->
                    norm ({cfg with steps=s; primitive_steps=ps; delta_level=dl}) env stack t
  
                  | MemoLazy r :: stack ->
                    set_memo r (env, t); //We intentionally do not memoize the strong normal form; only the WHNF
  
negative.code:     (* the Meta_monadic marker and reconstruct the computation after      *)
      (* normalization.                                                     *)
      let t = norm cfg env [] t in
      let stack = (Cfg cfg)::stack in
      let cfg =
        if cfg.steps |> List.contains PureSubtermsWithinComputations
        then
  