anchor.diff:  
     let dmff_env = DMFF.empty env (tc_constant env Range.dummyRange) in
     let wp_type = DMFF.star_type dmff_env repr in
  -  let wp_type = recheck_debug "*" env wp_type in
  +  let _ = recheck_debug "*" env wp_type in
     let wp_a = N.normalize [ N.Beta ] env (mk (Tm_app (wp_type, [ (S.bv_to_name a, S.as_implicit false) ]))) in
   
     // Building: [a -> wp a -> Effect]
  
positive.code:     if not (U.is_total_lcomp item_comp) then
        raise_err (Errors.Fatal_ComputationNotTotal, (BU.format2 "Computation for [%s] is not total : %s !" (Print.term_to_string item) (Print.lcomp_to_string item_comp)));
      let item_t, item_wp, item_elab = DMFF.star_expr dmff_env item in
      let item_wp = recheck_debug "*" env item_wp in
      let item_elab = recheck_debug "_" env item_elab in
      dmff_env, item_t, item_wp, item_elab
    in
  
  
negative.code:   t
  
  // A helper to check that the terms elaborated by DMFF are well-typed
  let recheck_debug s env t :term =
    if Env.debug env (Options.Other "ED") then
      BU.print2 "Term has been %s-transformed to:\n%s\n----------\n" s (Print.term_to_string t);
    let t', _, _ = tc_term env t in
    if Env.debug env (Options.Other "ED") then
      BU.print1 "Re-checked; got:\n%s\n----------\n" (Print.term_to_string t');
    t'
  
  
  let check_and_gen env t k =
  