Commit 12f1d315 authored by Andrei Paskevich's avatar Andrei Paskevich

export print_theory_tdecl in Pretty

parent 0e9334c1
......@@ -355,7 +355,7 @@ let print_named_task fmt name task =
fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
name (print_list newline2 print_task_tdecl) (task_tdecls task)
let print_th_tdecl fmt = function
let print_theory_tdecl fmt = function
| Theory.Decl d ->
print_decl fmt d
| Theory.Use th ->
......@@ -366,7 +366,7 @@ let print_th_tdecl fmt = function
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
print_th th (print_list newline2 print_th_tdecl) th.th_decls
print_th th (print_list newline2 print_theory_tdecl) th.th_decls
module NsTree = struct
type t =
......
......@@ -52,9 +52,11 @@ val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_task_tdecl : formatter -> Task.tdecl -> unit
val print_theory_tdecl : formatter -> Theory.tdecl -> unit
val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
......
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