aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2020-12-15Modify ZArith/Zgcd_alt.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpow_facts.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpower.v to compile with -mangle-namesJasper Hugunin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-11Modify ZArith/Znumtheory.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zdiv.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zpow_def.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Wf_Z.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zabs.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Znat.v to compile with -mangle-namesJasper Hugunin
2020-10-09Modify ZArith/ZArith_dec.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/Zorder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/BinInt.v to compile with -mangle-namesJasper Hugunin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zgcd_alt: use “lia” rather than “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-04-02Remove -compat 8.7Jason Gross
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:18 +0000