diff options
| -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. |