Commit 437d61c7 authored by Andrei Paskevich's avatar Andrei Paskevich

decorate terms in triggers

parent e93d20e9
......@@ -43,6 +43,10 @@ and deco_term kept tvar t = match t.t_node with
and deco_fmla kept tvar f = match f.f_node with
| Fapp (ps,tl) -> f_app ps (List.map (deco_arg kept tvar) tl)
| Fquant (q,b) ->
let vl,tl,f,close = f_open_quant_cb b in
let tl = tr_map (deco_arg kept tvar) (deco_fmla kept tvar) tl in
f_quant q (close vl tl (deco_fmla kept tvar f))
| _ -> f_map (deco_term kept tvar) (deco_fmla kept tvar) f
let deco_decl kept d = match d.d_node with
......
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