Libzipperposition_calculi.RewritingDeal with definitions as rewrite rules
module Make (E : Libzipperposition.Env_intf.S) : sig ... endval unfold_def_before_cnf :
((Logtk.TypedSTerm.t, Logtk.TypedSTerm.t, Logtk.TypedSTerm.t)
Logtk.Statement.t,
'c)
CCVector.t ->
((Logtk.TypedSTerm.t, Logtk.TypedSTerm.t, Logtk.TypedSTerm.t)
Logtk.Statement.t,
'c)
CCVector.tval extension : Libzipperposition.Extensions.t