• Sylvain Dailler's avatar
    Keeping keep_on_simp labels during wp generation. · 64b1fda4
    Sylvain Dailler authored
    We changed t_map_simp, track_values and the eval_match transformation
    in order to prevent them from removing terms whose head has label
     keep_on_simp. Note that simplification inside those terms is
    still possible.
    
    * src/core/term.ml
    (t_map_simp): Adding the case when f has label keep_on_simp.
    
    * src/transform/eval_match.ml
    (eval_match): Adding keep_on_simp as a stop label.
    
    * src/whyml/mlw_wp.ml
    (track_values): Stopping on keep_on_simp label.
    64b1fda4
Name
Last commit
Last update
..
decl.ml Loading commit data...
decl.mli Loading commit data...
dterm.ml Loading commit data...
dterm.mli Loading commit data...
env.ml Loading commit data...
env.mli Loading commit data...
ident.ml Loading commit data...
ident.mli Loading commit data...
model_parser.ml Loading commit data...
model_parser.mli Loading commit data...
pattern.ml Loading commit data...
pattern.mli Loading commit data...
pretty.ml Loading commit data...
pretty.mli Loading commit data...
printer.ml Loading commit data...
printer.mli Loading commit data...
task.ml Loading commit data...
task.mli Loading commit data...
term.ml Loading commit data...
term.mli Loading commit data...
theory.ml Loading commit data...
theory.mli Loading commit data...
trans.ml Loading commit data...
trans.mli Loading commit data...
ty.ml Loading commit data...
ty.mli Loading commit data...