module Trigger:sig
..end
val of_exp : Qed.Engine.cmode ->
Lang.F.term -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
val of_term : Lang.F.term -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
val of_pred : Lang.F.pred -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
val collect : Lang.F.Vars.t -> (Lang.F.Vars.elt, 'a) Qed.Engine.ftrigger -> Lang.F.Vars.t
val vars : (Lang.F.Vars.elt, Lang.lfun) Qed.Engine.ftrigger -> Lang.F.Vars.t