aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
AgeCommit message (Collapse)Author
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
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
(namely, [RewriteRelation]s beyond Equivalence ones) Thanks to @CohenCyril for suggesting this enhancement
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-21Improvements of zifyFrédéric Besson
- Fix reification of overloaded operators (triggers convertibility checks with existing terms) - Zify instances need not be in hnf - Fix specification of bool operators - Add (limited) support for comparison fixes #10779
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
Reviewed-by: herbelin
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
Prove that morphisms preserve additions Fix stdlib index Prove that constructive real morphisms preserve multiplications by integers Prove that constructive real morphisms preserve multiplications by rationals Prove CReal_mult_pos_appart_zero Prove that constructive real morphisms preserve multiplications Prove that constructive real morphisms preserve divisions Rewrite convergence in sort Prop, to extract smaller programs Rewrite convergence on integers, to extract smaller programs Fix typos
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:37:50 +0000