Relaxed the constraint introduced in r14190 that froze the existing

evars when rewriting. Use it for autorewrite and subst. Accept evars
instantiation in multi_rewrite so that rewrite alone remains
compatible (it is used in contribs, e.g. Godel, in places where it
does not seem absurd to allow it), but there are no good reason for
it. Comments welcome.
+ addition of some tests for rewriting (one being related to commit 14217)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b04f..ee09200573 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
 Set Implicit Arguments.
 
 Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
 Proof.
   intros Env A e p; eapply ex_intro.
   autorewrite with placeeq. (* Here is the bug *)
-  auto.
-Qed.
 
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce73..5e9064f8af 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
     apply H;reflexivity.
 Qed.
 
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
 
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe78..3d49d3cf93 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,14 @@ intros.
 rewrite (H _).
 reflexivity.
 Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+   argument of the goal. This is sometimes used in contribs, even if
+   ad hoc. Here, we have the extra requirement that checking types
+   needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+