• Guillaume Melquiond's avatar
    Fix incorrect usage of t_fold. · cb5c96e7
    Guillaume Melquiond authored
    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.
    cb5c96e7
Name
Last commit
Last update
..
abstraction.ml Loading commit data...
abstraction.mli Loading commit data...
close_epsilon.ml Loading commit data...
close_epsilon.mli Loading commit data...
discriminate.ml Loading commit data...
discriminate.mli Loading commit data...
eliminate_algebraic.ml Loading commit data...
eliminate_algebraic.mli Loading commit data...
eliminate_definition.ml Loading commit data...
eliminate_definition.mli Loading commit data...
eliminate_if.ml Loading commit data...
eliminate_if.mli Loading commit data...
eliminate_inductive.ml Loading commit data...
eliminate_inductive.mli Loading commit data...
eliminate_let.ml Loading commit data...
eliminate_let.mli Loading commit data...
encoding.ml Loading commit data...
encoding.mli Loading commit data...
encoding_decorate.ml Loading commit data...
encoding_decorate.mli Loading commit data...
encoding_explicit.ml Loading commit data...
encoding_explicit.mli Loading commit data...
encoding_guard.ml Loading commit data...
encoding_instantiate.ml Loading commit data...
encoding_instantiate.mli Loading commit data...
encoding_select.ml Loading commit data...
encoding_select.mli Loading commit data...
encoding_sort.ml Loading commit data...
encoding_twin.ml Loading commit data...
encoding_twin.mli Loading commit data...
eval_match.ml Loading commit data...
eval_match.mli Loading commit data...
filter_trigger.ml Loading commit data...
hypothesis_selection.ml Loading commit data...
inlining.ml Loading commit data...
inlining.mli Loading commit data...
instantiate_predicate.ml Loading commit data...
introduction.ml Loading commit data...
introduction.mli Loading commit data...
libencoding.ml Loading commit data...
libencoding.mli Loading commit data...
lift_epsilon.ml Loading commit data...
lift_epsilon.mli Loading commit data...
protect_enumeration.ml Loading commit data...
protect_enumeration.mli Loading commit data...
simplify_array.ml Loading commit data...
simplify_formula.ml Loading commit data...
simplify_formula.mli Loading commit data...
simplify_recursive_definition.ml Loading commit data...
simplify_recursive_definition.mli Loading commit data...
split_goal.ml Loading commit data...
split_goal.mli Loading commit data...