diff options
| author | Hugo Herbelin | 2015-02-23 12:43:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-23 12:50:45 +0100 |
| commit | 06ad2a73251f38c59c43c03a0edca34d5ef3dd8e (patch) | |
| tree | 7f74e8e7ffc3e1129c530a49f2cc23d031962972 | |
| 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?
| -rw-r--r-- | pretyping/unification.ml | 7 | ||||
| -rw-r--r-- | test-suite/success/rewrite.v | 10 |
2 files changed, 16 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 99c20ef6ce..01e1154e58 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1780,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = try (* This is up to delta for subterms w/o metas ... *) w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) - with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op) + with PretypeError (env,_,NoOccurrenceFound _) when + allow_K || + (* w_unify_to_subterm does not go through evars, so + the next step, which was already in <= 8.4, is + needed at least for compatibility of rewrite *) + dependent op t -> (evd,op) in if not allow_K && (* ensure we found a different instance *) diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 6dcd6592b5..62249666b3 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. |