Module Vc

module Vc: sig .. end

val sp_attr : Ident.attribute
val wp_attr : Ident.attribute
val kp_attr : Ident.attribute
val wb_attr : Ident.attribute
val nt_attr : Ident.attribute
val set_infer_invs : (Ident.Sattr.t ->
Env.env ->
Decl.known_map ->
Pdecl.known_map -> Expr.expr -> Ity.cty -> (Expr.expr * Term.term) list) ->
unit
val vc : Env.env ->
Pdecl.known_map -> Theory.theory_uc -> Pdecl.pdecl -> Pdecl.pdecl list