diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-24 19:56:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-25 10:39:12 +0100 |
| commit | f4a8b00fa0ca47ef7dce4ca2ca809ef4ac440d38 (patch) | |
| tree | 50819ce6170a495c424f1e8b90ac9ad58f846782 /test-suite/success | |
| 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')
| -rw-r--r-- | test-suite/success/rewrite.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index f7b9897c1..6dcd6592b 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -139,3 +139,12 @@ subst z. rewrite H0. auto with arith. Qed. + +(* Check that evars are instantiated when the term to rewrite is + closed, like in the case it is open *) + +Goal exists x, S 0 = 0 -> S x = 0. +eexists. intro H. +rewrite H. +reflexivity. +Abort. |