Commit bf4646f0 authored by MARCHE Claude's avatar MARCHE Claude

parameters of logic fun were not forgotten by alt-ergo printer

parent 0581387b
......@@ -61,7 +61,7 @@ let tv_set = ref Sid.empty
(* type variables always start with a quote *)
let print_tv fmt tv =
tv_set := Sid.add tv !tv_set;
let sanitize n = String.concat "" ["'"; n] in
let sanitize n = "'" ^ n in
let n = id_unique iprinter ~sanitizer:sanitize tv in
fprintf fmt "%s" n
......
......@@ -189,7 +189,7 @@ let print_logic_decl drv ctxt fmt = function
fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl (print_fmla drv) f;
true
List.iter forget_var vl;true
end
let print_decl drv ctxt fmt d = match d.d_node with
......
......@@ -62,7 +62,7 @@ let tv_set = ref Sid.empty
(* type variables always start with a quote *)
let print_tv fmt tv =
tv_set := Sid.add tv !tv_set;
let sanitize n = String.concat "" ["'"; n] in
let sanitize n = "'" ^ n in
let n = id_unique iprinter ~sanitizer:sanitize tv in
fprintf fmt "%s" n
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment