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