aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Expand)Author
2020-08-25Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMul.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZAdd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZBase.v to compile with -mangle-namesJasper Hugunin
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
2020-08-09Bring Int63 notations into line with stdlibJason Gross
2020-05-09Hexadecimal: conversion to/from Coq stringsPierre Roux
2020-05-09Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijectionsPierre Roux
2020-05-09Decimal: prove numeral notation for QPierre Roux
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-09Uniformize indentation in theories/NumbersPierre Roux
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-05-04add order properties about boolOlivier Laurent
2020-04-19Fix a typoPierre Roux
2020-04-08Merge PR #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
2020-03-25Make the level of ≡ in Int63 consistent with =Jason Gross
2020-03-24[stdlib] Do not rely on failing “auto”Vincent Laporte
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-26Consolidate int63-related notationsMaxime Dénès
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes #1...Maxime Dénès
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard impleme...thery
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
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-11-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-22Fix typo in comment.Nick Lewycky
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:33 +0000