aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
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
2017-02-15Added some theory on powerRZ.Thomas Sibut-Pinote
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-08-18Fix an occurrence of deprecated eqn syntax in stdlib.Maxime Dénès
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 14:16:54 +0000