aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
AgeCommit message (Expand)Author
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
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-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:02:52 +0000