sig
  val hk : bool Pervasives.ref
  val congruence : bool Pervasives.ref
  val ssf : bool Pervasives.ref
  val trace : bool Pervasives.ref
  val construction : [ `Antimirov | `Brzozowski | `IlieYu ] Pervasives.ref
  val equiv :
    ?hyps:Hypotheses.t -> Kat.expr -> Kat.expr -> Kat.gstring option
  val compare :
    ?hyps:Hypotheses.t ->
    Kat.expr ->
    Kat.expr ->
    (Kat.expr' * Kat.expr') *
    [ `D of Kat.gstring * Kat.gstring
    | `E
    | `G of Kat.gstring
    | `L of Kat.gstring ]
  val check :
    [ `D | `E | `G | `L ] -> ?hyps:string -> string -> string -> unit
end