anchor.diff:      let (ts, cs) =
           let fold1 sigelt (types, ctors) =
               match sigelt with
  -            | Sig_tycon (x, tps, k, ts, cs, qualif, rg) -> begin
  +            | Sig_tycon (x, tps, k, ts, cs, qualif, rg) ->
  +              if List.contains Logic qualif then (types, ctors)
  +              else begin
                   let ar =
                       match mlkind_of_kind tps k with
                       | None    -> unsupported rg "not-an-ML-kind"
  
positive.code:     | Sig_monads (_, _, rg, _) ->
          unsupported rg "mod1-monad"
  
      | Sig_bundle ([Sig_datacon (x, ty, (tx, _, _), _, rg)], _, _) when (as_tprims tx = Some Exn) -> begin
          let rec aux acc ty =
              match (Absyn.Util.compress_typ ty).n with
              | Typ_fun(bs, c) -> 
  
negative.code:         | Inl ({v=x; sort={n=Kind_type}}), _ -> Some (x.realname, x.ppname)
  //        | Inr ({v=x}), _ -> Some (x.realname, x.ppname)
  //        | Inr ({sort={n=Typ_const {v=x; sort={n=Kind_type}}}}), _ -> Some (x.ident, x.ident)
          | x -> None // Util.print_any x; None
      in
  
      let rec aux acc (k : knd) =
  