aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
AgeCommit message (Expand)Author
2019-10-21Improvements of zifyFrédéric Besson
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-09-16Re-implementation of zifyFrédéric Besson
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
2019-07-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-04-02Remove -compat 8.7Jason Gross
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
2019-02-04Primitive integersMaxime Dénès
2019-01-24Update -compat to support -compat 8.10Jason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-16Merge PR #8888: Proof runcountable rebaseHugo Herbelin
2018-11-07[doc] also scan plugins/ to build the lirbary indexEnrico Tassi
2018-11-01Fix header and doc indexVincent Semeria
2018-10-17doc: mention ByteVectorYishuai Li
2018-10-02Update the -compat flagsJason Gross
2018-08-31Numeral Notation for natPierre Letouzey
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-02-20Doc: add Decimal-related files to index-list.html.templateJason Gross
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
2016-06-03Fix build of documentation (broken for four months).Guillaume Melquiond
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-10-02Mark the Coq.Compat files for documentation. (Fix bug #4353)Guillaume Melquiond
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-04-02Fix compilation of documentation broken by the addition of MMapAVL.Guillaume Melquiond
2015-03-21Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Guillaume Melquiond
2014-12-09doc/stdlib: fix the xhtml validity of the index-list templatePierre Letouzey
2014-12-09Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...notin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:57:23 +0000