aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-10Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else fa...Vincent Semeria
2019-08-09Switch constructive Rlt to sort Type, to make it compute laterVincent Semeria
2019-08-08Fix namespace of Cauchy realsVincent Semeria
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-06Prove the completeness of real numbers from logical axiom sig_not_decVincent Semeria
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-07-26Fix typoVincent Semeria
2019-07-24changed name of cos3PI4 to cos_3PI4 for consistencyRobert Rand
2019-07-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-07Improve field_simplify on fractions with constant denominatorthery
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-19Merge PR #8987: Deprecate hint declaration/removal with no specified databasePierre-Marie Pédrot
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-11-01develop constructive epsilonVincent Semeria
2018-11-01Fix header and doc indexVincent Semeria
2018-11-01proof that R is uncountableVincent Semeria
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-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-07-17Remove fourier pluginMaxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-28Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-06weakens an hypothesis of Rle_RpowerYves Bertot
2017-09-06changed statements of Rpower_lt and Rle_power and addedYves Bertot
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Remove deprecated options from the standard library.Guillaume Melquiond
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-04-29Suppress warning message in stdlib.Guillaume Melquiond
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-07Add some hints to the "real" database to automatically discharge literal comp...Guillaume Melquiond
2017-04-02Fix documentation typo (bug #5433).Guillaume Melquiond
2017-04-02Simplify some proofs.Guillaume Melquiond
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-03-22Make IZR use a compact representation of integers.Guillaume Melquiond
2017-03-22Simplify some proofs using ring and field.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:19:49 +0000