Commit fdf7d1c3 authored by Francois Bobot's avatar Francois Bobot
Browse files

--print-namespace : ajout de type, logic et prop

parent cdf7be7f
......@@ -187,9 +187,10 @@ let print_theory_namespace fmt th =
let acc =
Mnm.fold (fun s ns acc -> (Namespace (s, ns)) :: acc) ns.ns_ns []
in
let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_ts acc in
let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_ls acc in
let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_pr acc in
let add prefix = Mnm.fold (fun s _ acc -> (Leaf (prefix^s)) :: acc) in
let acc = add "type " ns.ns_ts acc in
let acc = add "logic " ns.ns_ls acc in
let acc = add "prop " ns.ns_pr acc in
acc
let decomp = function
| Namespace (s, ns) -> s, contents ns
......
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