anchor.diff:                      then AST.ml_comp t
                       else AST.tot_comp t
                   in
  -                mk_term (Ascribed(def, t, tacopt)) def.range Expr
  +                mk_term (Ascribed(def, t, tacopt, false)) def.range Expr
               in
               let def = match args with
                    | [] -> def
  
positive.code:         match bs with
          | [] ->
            let sq_p = U.mk_squash U_unknown p in
            U.ascribe e (Inl sq_p, None)
  
          | b::bs ->
            let tail = aux bs in
  
negative.code:       | Some b ->
          let env, bv = Env.push_bv env b in
          env, S.mk_binder bv in
      let asc, aq = desugar_ascription env_asc asc_tc None asc_use_eq in
      //if scrutinee is a name, it may appear in the ascription
      //  substitute it with the (new or annotated) binder
      let asc =
  