| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: anton-trunov
|
|
Reviewed-by: cpitclaudel
|
|
[stdlib] Add changelog for PR #11335
|
|
Ack-by: MSoegtropIMC
Ack-by: Zimmi48
Ack-by: herbelin
|
|
[stdlib] Add complementary results about Permutation
|
|
|
|
Reviewed-by: Lysxia
Reviewed-by: Zimmi48
|
|
|
|
- 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)
|
|
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r`
- sin : sin_inj
- cos : cos_inj
- sqrt : lemmas `pow2_sqrt` and `inv_sqrt`
- atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan`
- asin : definition and some basic properties
- acos : definition and some basic properties
|
|
|
|
Reviewed-by: ejgallego
|
|
NArith, PArith: Add facts about iter
|
|
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
|
|
The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook
We handle this automatically now; it seems like a reasonably good API
improvement.
However, it is not clear what we do now is right for all cases; must
check.
|
|
Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.
This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:
- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
|
|
Fix makefile glitches
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
|
|
Use `dune build @check-gram --auto-promote` to automatically update
these two files. You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.
The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory. You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
|
|
|
|
|
|
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
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: maximedenes
|
|
This octopus merge is meant to preserve the commit history / blame of
both parts.
|
|
|
|
(It was moved out onto a separate page.)
|
|
|
|
one. Fix build of PDF manual.
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
As CIC is really an acronym, it should be printed in all-caps.
|
