module VC_Annot:sig
..end
type
t = {
|
axioms : |
|
goal : |
|
: |
|
warn : |
|
deps : |
|
path : |
|
effect : |
}
val is_trivial : t -> bool
val resolve : pid:Wp.WpPropId.prop_id -> t -> bool
val cache_descr : pid:Wp.WpPropId.prop_id ->
t -> (Wp.VCS.prover * Wp.VCS.result) list -> string