Commit 62029d77 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed PVS output (all types are non empty)

parent 01f936d6
...@@ -249,7 +249,7 @@ theory list.List ...@@ -249,7 +249,7 @@ theory list.List
syntax type list "list[%1]" syntax type list "list[%1]"
syntax function Nil "null" syntax function Nil "(null :: %t0)"
syntax function Cons "cons(%1, %2)" syntax function Cons "cons(%1, %2)"
end end
......
...@@ -124,7 +124,7 @@ let print_tv fmt tv = ...@@ -124,7 +124,7 @@ let print_tv fmt tv =
let print_tv_binder fmt tv = let print_tv_binder fmt tv =
tv_set := Sid.add tv.tv_name !tv_set; tv_set := Sid.add tv.tv_name !tv_set;
let n = id_unique iprinter tv.tv_name in let n = id_unique iprinter tv.tv_name in
fprintf fmt "%s:TYPE" n fprintf fmt "%s:TYPE+" n
let print_params_list fmt = function let print_params_list fmt = function
| [] -> () | [] -> ()
...@@ -628,7 +628,7 @@ let print_type_decl ~prev info fmt ts = ignore (prev); ...@@ -628,7 +628,7 @@ let print_type_decl ~prev info fmt ts = ignore (prev);
realization fmt info prev; realization fmt info prev;
fprintf fmt "@]@\n@\n" fprintf fmt "@]@\n@\n"
| Some ty -> | Some ty ->
fprintf fmt "@[<hov 2>%a%a: TYPE =@ %a@]@\n@\n" fprintf fmt "@[<hov 2>%a%a: TYPE+ =@ %a@]@\n@\n"
print_ts ts print_params_list ts.ts_args print_ts ts print_params_list ts.ts_args
(print_ty info) ty (print_ty info) ty
end end
......
Supports Markdown
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