diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-16 18:17:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-16 18:17:45 +0000 |
| commit | 5297477d29c7e80ce1a6a2cb9d0fc61fcee3a651 (patch) | |
| tree | 589484cc1534d0812c451a5a04081fe115f779e5 /theories/Numbers/NatInt/NZDomain.v | |
| parent | 2c2a1b91e994a4256d1bbebaa405ad114d834206 (diff) | |
Univ: two improvements (speed + space)
- The "compare" function on universes (the one answering EQ|LT|LE|NLE)
was launching "collect" for creating the transitive upward closure
of u, and then checking if v is in it. We now proceed more lazily,
by stopping creating the transitive closure as soon as v is found.
- In univ_entry, the first arg u of Equiv(u,v) is removed. It can
indeed be retrieved from the key of the universe graph leading
to this Equiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt/NZDomain.v')
0 files changed, 0 insertions, 0 deletions