From fe3db6e9f688af4c9da29f6508c285bf42324eab Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Apr 2010 22:01:23 +0000
Subject: Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which
 was actually failing for another reason than the reason originally filled in
 the bug tracker) and revealed a bug in the unification.v test file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/1416.v | 27 +++++++++++++++++++++++++++
 test-suite/bugs/opened/shouldnotfail/1416.v | 27 ---------------------------
 2 files changed, 27 insertions(+), 27 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1416.v
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1416.v

diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
new file mode 100644
index 0000000000..da67d9b04f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -0,0 +1,27 @@
+Set Implicit Arguments.
+
+Record Place (Env A: Type) : Type := {
+  read: Env -> A ;
+  write: Env -> A -> Env ;
+  write_read: forall (e:Env), (write e (read e))=e
+}.
+
+Hint Rewrite -> write_read: placeeq.
+
+Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
+ {
+   mkEnv: A -> B -> Env ;
+   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
+ }.
+
+(* when the following line is commented, the bug does not appear *)
+Hint Rewrite -> mkEnv2writeL: placeeq.
+
+Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
+  (exists e1:Env, e=(write p e1 (read p e))).
+Proof.
+  intros Env A e p; eapply ex_intro.
+  autorewrite with placeeq. (* Here is the bug *)
+  auto.
+Qed.
+
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v
deleted file mode 100644
index da67d9b04f..0000000000
--- a/test-suite/bugs/opened/shouldnotfail/1416.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Set Implicit Arguments.
-
-Record Place (Env A: Type) : Type := {
-  read: Env -> A ;
-  write: Env -> A -> Env ;
-  write_read: forall (e:Env), (write e (read e))=e
-}.
-
-Hint Rewrite -> write_read: placeeq.
-
-Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
- {
-   mkEnv: A -> B -> Env ;
-   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
- }.
-
-(* when the following line is commented, the bug does not appear *)
-Hint Rewrite -> mkEnv2writeL: placeeq.
-
-Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
-  (exists e1:Env, e=(write p e1 (read p e))).
-Proof.
-  intros Env A e p; eapply ex_intro.
-  autorewrite with placeeq. (* Here is the bug *)
-  auto.
-Qed.
-
-- 
cgit v1.2.3