diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 22:42:23 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 22:42:23 +0000 |
| commit | 49a7bb129b8a7f9d5a9175b7a340112c20e95d96 (patch) | |
| tree | 6205fc798ab6b996d1188f7492721d3c0247722f /theories/Numbers/NumPrelude.v | |
| parent | 972a60b36778a5c6971aa3f9a72073fd19f02b84 (diff) | |
In practice, the new setoid rewrite (and the "at" syntax) allows to avoid
using the ad-hoc qsetoid_rewrite. Could QRewrite.v be made completely obsolete ?
For the moment rewrite under fun and exists don't work.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10935 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NumPrelude.v')
| -rw-r--r-- | theories/Numbers/NumPrelude.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 2c221a88e..f2f6b9082 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -11,11 +11,6 @@ (*i $Id$ i*) Require Export Setoid. -(*Require Export Bool.*) -(* Standard library. Export, not Import, because if a file -importing the current file wants to use. e.g., -Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2, -then it needs to know about bool and have a notation ||. *) Require Export QRewrite. Set Implicit Arguments. @@ -183,7 +178,7 @@ let x2 := fresh "x" in let y2 := fresh "y" in let H2 := fresh "H" in intros x1 y1 H1 x2 y2 H2; - qsetoid_rewrite H1; + rewrite H1; qiff x2 y2 H2. (* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite |