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?

Author: herbelin

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 *)

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.