aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
AgeCommit message (Collapse)Author
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
add polynomial specifications of to_nat add changelog and doc entries
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
Reviewed-by: JasonGross Reviewed-by: MSoegtropIMC
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-01-22Add a type of format strings to Ltac2.Pierre-Marie Pédrot
It provides an abstract type of well-typed format strings, a scope to parse them and a minimal printf-like API.
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-05[numeral notation] Specify RPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-09Hexadecimal: conversion to/from Coq stringsPierre Roux
2020-05-09Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijectionsPierre Roux
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-04add order properties about boolOlivier Laurent
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
Ack-by: Zimmi48 Ack-by: anton-trunov Reviewed-by: herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-19A library on cyclic permutations: CPermutationOlivier Laurent
(following the pattern of Permutation.v)
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-05Adding package amssymb to support \lessgtr (apartness) in LaTeX output of ↵Hugo Herbelin
coqdoc.
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
2020-03-27Merge PR #11751: Fix #11749: don't warn for hidden files.Maxime Dénès
Reviewed-by: maximedenes
2020-03-23Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.Frédéric Besson
Reviewed-by: fajb
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
Also tweak the changelog entry to explain the difference.
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
Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003
2020-02-08Remove -compat 8.9.Théo Zimmermann
Commit auto-generated by running dev/tools/update-compat.py --release. As per release doc this must be run at some point before branching (not necessarily close to the branching date).
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
This partially fixes #10139 ; we now build the Ltac2 documentation and deploy it. The fix here can be used for inspiration to do the make-based part.
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
As suggested during review. That's a much better name.
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:19:17 +0000