aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Expand)Author
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
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Merge PR #8230: fix formulation of the Euclid Theorem in commentHugo Herbelin
2018-09-10Declaring Scope prior to loading primitive printers.Hugo Herbelin
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
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31Numeral Notation for natPierre Letouzey
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-08-10one more fix to formulation of the Euclid Theorem in commentSamuel Gruetter
2018-08-09fix formulation of the Euclid Theorem in commentSamuel Gruetter
2018-07-16Ascii.eqb and String.eqbPierre Letouzey
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Decimal goodies : conversion to/from Coq stringsPierre Letouzey
2018-02-20Decimal: proofs that conversions from/to nat,N,Z are bijectionsPierre Letouzey
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-26Merge PR #845: Add Z.mod_div lemma to standard library.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-29Add Z.mod_div lemma to standard library.Russell O'Connor
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-09-28ZDivEucl: notations in different scope to avoid a warningPierre Letouzey
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16Remove unneded hints in NZGcdMatthieu Sozeau
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-06-16In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04NPeano : improve compatibility for this deprecated file via compat notationsPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 18:38:04 +0000