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/Natural/BigN/BigN.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/Natural/BigN/BigN.v')
0 files changed, 0 insertions, 0 deletions