aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
AgeCommit message (Expand)Author
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...Vincent Semeria
2020-03-27Merge PR #11751: Fix #11749: don't warn for hidden files.Maxime Dénès
2020-03-23Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.Frédéric Besson
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
2020-03-20Build and install refman with Dune.Théo Zimmermann
2020-03-04Fix #11749: don't warn for hidden files.Théo Zimmermann
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:30:28 +0000