aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-02-28Fix #7632: Change syntax of autoapply according to the documentation.Théo Zimmermann
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-04Enrich implicits for instancesJasper Hugunin
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-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-12-12Merge PR #9087: Add CI job building stdlib with `async-proofs on`Emilio Jesus Gallego Arias
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Avoid Fixpoint without struct nor body in stdlibMaxime Dénès
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-11-30Merge PR #8807: Added two proofs to the Lists library: Forall_inv_tail and Ex...Pierre-Marie Pédrot
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Proofs to ensure that conversions round-tripJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends Fo...llee454@gmail.com
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:40:31 +0000