Restore build [skip ci]

This commit is contained in:
Denis Merigoux 2022-01-18 17:59:15 +01:00
parent 777f194178
commit 2e1dc4740a
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -22,6 +22,8 @@ type vc_return = expr Pos.marked * typ Pos.marked VarMap.t
(** The return type of VC generators is the VC expression plus the types of any locally free
variable inside that expression. *)
type ctx = { decl : decl_ctx; input_vars : Var.t list }
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
match args with hd :: tl -> (hd, tl) | [] -> (((ELit (LBool true), pos), VarMap.empty), [])
@ -96,8 +98,6 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
e)
(Pos.get_position e)
type ctx = { decl : decl_ctx; input_vars : Var.t list }
(** {1 Verification conditions generator}*)
(** [generate_vc_must_not_return_empty e] returns the dcalc boolean expression [b] such that if [b]