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

0 files changed, 0 insertions, 0 deletions