CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Match annotation type in io.mli and in Z3 backend

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-09-12 18:10:02 +02:00
parent 0592cdab2a
commit ea13981c5d
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
compiler/verification/z3backend.real.ml
View File

@ -626,7 +626,7 @@ let rec translate_op (ctx : context) (op : operator) (args : 'm expr list) :
(** [translate_expr] translate the expression [vc] to its corresponding Z3
expression **)
and translate_expr (ctx : context) (vc : 'm expr) : context * Expr.expr =
and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
let translate_match_arm
(head : Expr.expr)
(ctx : context)
@ -817,7 +817,7 @@ module Backend = struct
let is_model_empty (m : model) : bool = List.length (Z3.Model.get_decls m) = 0
let translate_expr (ctx : backend_context) (e : 'm expr) =
let translate_expr (ctx : backend_context) (e : typed expr) =
translate_expr ctx e
let init_backend () =