module CfgWP: sig .. end
sig
end
module WpLog: Wp_parameters
Wp_parameters
module VC: functor (M : Memory.Model) -> sig .. end
functor (
M
:
Memory.Model
) ->
val add_qed_check : Wpo.t Bag.t Pervasives.ref -> Model.t -> qed:Lang.F.t -> raw:Lang.F.t -> goal:Lang.F.pred -> unit
Wpo.t Bag.t Pervasives.ref -> Model.t -> qed:Lang.F.t -> raw:Lang.F.t -> goal:Lang.F.pred -> unit
module Computer: functor (M : Memory.Model) -> sig .. end