Merge branch 'build' into integration
Added the Coq representation of ML integers.

ML integers (int) are mapped from Z binary numbers. Obviously, this
mapping is incorrect but it should be sufficient for the compilation
purpose.
Added the [int] syntactic sugar.
Added the src/mltypes/int.v file to targets.
Merge branch 'integer' into integration
Added Setoid definition.
Added src/math/setoid.v to targets.
Merge branch 'math' into integration
Renaming the math stuf to follow the capitalized module convention.
Added a PartialOrder definition.
Merge branch 'math' into integration
Merge branch 'build' into integration
Merge branch 'integration' into math
Added TotalOrder class with related instances.
Merge branch 'math' into integration
Merge branch 'integration' into integer
Renamed the mltypes directory according to the usual Coq naming
conventions.
Reword some doc.
Added base arithmetic operations and rewrote the coercion from Z with them.
Renamed operations to define ordering instances.