aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/numCompat.ml
AgeCommit message (Collapse)Author
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-04[micromega] Add numerical compatibility layer.Emilio Jesus Gallego Arias
Only significant change is in gcd / lcm which now are typed in `Z.t`