DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation

 - Records of operations and specs in CyclicAxioms are now
   type classes (under a module ZnZ for qualification).
   We benefit from inference and from generic names:
   (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y).

 - Beware of typeclasses unfolds: the line about
   Typeclasses Opaque w1 w2 ... is critical for decent
   compilation time (x2.5 without it).

 - Functions defined via same_level are now obtained from a
   generic version by (Eval ... in ...) during definition.
   The code obtained this way should be just as before, apart
   from some (minor?) details. Proofs for these functions
   are _way_ simplier and lighter.

 - The macro-generated NMake_gen.v contains only generic iterators
   and compare, mul, div_gt, mod_gt. I hope to be able to adapt
   these functions as well soon.

 - Spec of comparison is now fully done with respect to Zcompare

 - A log2 function has been added.

 - No more unsafe_shiftr, we detect the underflow directly with sub_c

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions