diff options
author | 2014-11-24 19:56:00 +0100 | |
---|---|---|
committer | 2014-11-25 10:39:12 +0100 | |
commit | f4a8b00fa0ca47ef7dce4ca2ca809ef4ac440d38 (patch) | |
tree | 50819ce6170a495c424f1e8b90ac9ad58f846782 /test-suite/success/Simplify_eq.v | |
parent | c8852c570c980e35072ff40c84c375f84ec5f581 (diff) |
Experimenting using unification when matching evar/meta free subterms
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
Diffstat (limited to 'test-suite/success/Simplify_eq.v')
0 files changed, 0 insertions, 0 deletions