Commit cb5c96e7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix incorrect usage of t_fold.

t_fold already iters on the subterms of a term, so calling t_fold on a
subterm actually iters over grandchildren of the term, which may well be
under a quantifier. So t_fold should be called on the term itself.

This explains why the transformation was trying to create declarations with
unbounded variables.
parent 339a7732
......@@ -44,12 +44,10 @@ let trans spr task_hd (((lpr, past), task) as current) =
) lpr task
) in
match t.t_node with
| Tapp _ ->
| Tapp _
| Tbinop _
| Tnot _ ->
t_fold scan_term current t
| Tbinop (_,f1,f2) ->
t_fold scan_term (t_fold scan_term current f1) f2
| Tnot f ->
t_fold scan_term current f
| _ -> current in
let (current, task) =
......
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