aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Expand)Author
2020-10-08Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZGcd.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivFloor.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivTrunc.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZSgnAbs.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-namesJasper Hugunin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-08-25Modify Numbers/NatInt/NZGcd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZDiv.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZLog.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZPow.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZParity.v to compile with -mangle-namesJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-11 20:42:13 +0000