diff options
author | 2015-02-23 12:43:01 +0100 | |
---|---|---|
committer | 2015-02-23 12:50:45 +0100 | |
commit | 06ad2a73251f38c59c43c03a0edca34d5ef3dd8e (patch) | |
tree | 7f74e8e7ffc3e1129c530a49f2cc23d031962972 /test-suite/success | |
parent | 71def2f885989376c8c2940d37f7fc407ed0a4c5 (diff) |
Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.
This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/rewrite.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 6dcd6592b..62249666b 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -148,3 +148,13 @@ eexists. intro H. rewrite H. reflexivity. Abort. + +(* Check that rewriting within evars still work (was broken in 8.5beta1) *) + + +Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y. +intros; eexists; eexists. +rewrite H. +Undo. +subst. +Abort. |