diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-09 20:04:43 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-09 20:04:43 +0000 |
commit | 97e46c18bb207726cfc42f25fc901772579d7057 (patch) | |
tree | 89ec6b1fa38fd5341ea8c8039804634632a92c1a /checker | |
parent | 015e33fb137c89ba96b2806f828cd47341c3bd92 (diff) |
NMake : another round of heavy rework
- generic iterator [iter] factorized in the same way as [same_level]
- as a consequence, remaining operations [mul] [compare] [div_gt]
are now defined and proved in a short and nice way and moved to
NMake.v.
- lots of other simplifications / factorisations in NMake_gen.
This file is still macro-generated, but is much shorter,
and the major part of it is now invariant.
- As advised by B. Gregoire, try to (re)create clever partial
applications in code of operators, in order to avoid projecting
ZnZ fields all the time in base cases. Case 0 can still be improved,
but it's already better this way :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions