Commit 4b8f1cff authored by Andrei Paskevich's avatar Andrei Paskevich

simplify_trivial_quant removes quantifiers over unused variables

parent 3a9ea01e
......@@ -113,7 +113,9 @@ let rec fmla_quant ~keep_model_vars sign f = function
| vs::l ->
let vsl, f = fmla_quant ~keep_model_vars sign f l in
if keep_model_vars && has_a_model_attr vs.vs_name then
vs::vsl, f
vs::vsl, f
else if t_v_occurs vs f = 0 then
vsl, f
else
try
fmla_find_subst (Svs.singleton vs) vs sign f;
......
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