diff options
author | 2007-08-22 15:08:31 +0000 | |
---|---|---|
committer | 2007-08-22 15:08:31 +0000 | |
commit | f5a03a037e9773d7be90ac50500e70245f5fec3c (patch) | |
tree | d99bca9f8ca41f3b7593e0e0826e59a367172d97 /test-suite/bugs/opened | |
parent | 0014a18c28c3d601c61eb453b3936461c7c16bd8 (diff) |
Correction du bug #1634 + ajout de bugs dans la test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1416.v | 27 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/743.v | 12 |
2 files changed, 39 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v new file mode 100644 index 000000000..c6f4302d8 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/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/743.v b/test-suite/bugs/opened/shouldnotfail/743.v new file mode 100644 index 000000000..f1eee6c18 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/743.v @@ -0,0 +1,12 @@ +Require Import Omega. + +Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z. +Proof. + intros. omega. +Qed. + +Lemma foo' : forall n m : nat, n <= n + n * m. +Proof. + intros. omega. +Qed. + |