aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-25Make Bool.eqb_spec transparentTej Chajed
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-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
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-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-27Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distrHugo Herbelin
2019-07-26Fix typoVincent Semeria
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
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-20Fix coqdoc title: should be on a single line.Théo Zimmermann
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-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...Maxime Dénès
2019-05-07Improve field_simplify on fractions with constant denominatorthery
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-05-01Add PairUsualDecidableTypeFullOliver Nash
2019-04-08Fix spelling in comment.nlewycky
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)Pierre Roux
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
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
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 12:57:17 +0000