index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2020-04-02
Remove deprecated -require option.
Théo Zimmermann
2020-04-02
Merge pull request #11993 from olaure01/ollibs-wfnat-changelog
Anton Trunov
2020-04-01
Merge PR #9803: Adding more trigonometry in Reals
Hugo Herbelin
2020-04-01
Merge pull request #11946 from olaure01/ollibs-permutation
Anton Trunov
2020-04-01
Merge PR #10592: coqdoc: Add a new `details' environment for coqdoc
Lysxia
2020-04-01
Add changelog for PR #11335
Olivier Laurent
2020-04-01
- Adjusted definitions and lemmas for asin and acos to what has been discussed
Michael Soegtrop
2020-04-01
- Addition to the Reals theory :
thery
2020-04-01
Add complementary results about Permutation
Olivier Laurent
2020-04-01
Merge PR #11960: Docgram use new no update option
Emilio Jesus Gallego Arias
2020-04-01
Merge pull request #11880 from Lysxia/iter
Anton Trunov
2020-03-31
NArith, PArith: Add facts about iter
Lysxia
2020-03-31
Include review suggestions
Gaëtan Gilbert
2020-03-31
Remove special case for implicit inductive parameters
Maxime Dénès
2020-03-31
Merge PR #11818: [proof] Further consolidation of the regular declaration path
Gaëtan Gilbert
2020-03-31
Merge PR #11131: [ci] [gitlab] Add test-suite test for OCaml 4.10 and 4.11
Théo Zimmermann
2020-03-30
[declare] Fuse prepare and declare for the non-interactive path.
Emilio Jesus Gallego Arias
2020-03-30
[declareDef] More consistent handling of universe binders
Emilio Jesus Gallego Arias
2020-03-30
[declare] [obligations] Refactor preparation of obligation entry
Emilio Jesus Gallego Arias
2020-03-30
Merge PR #11725: Cleanup stdlib reals.
Hugo Herbelin
2020-03-30
[dune] [docgram] Remove bash hack thanks to new option -no-update.
Théo Zimmermann
2020-03-30
Merge PR #11958: Add -no-update command line option to doc_grammar for Dune
Théo Zimmermann
2020-03-30
Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”
Maxime Dénès
2020-03-29
[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11
Emilio Jesus Gallego Arias
2020-03-29
Add -no-update command line option to doc_grammar for Dune
Jim Fehrle
2020-03-29
Merge PR #11938: Support for updating orderedGrammar with Dune.
Emilio Jesus Gallego Arias
2020-03-29
Merge PR #11859: Warn when non exactly parsing non floating-point
Hugo Herbelin
2020-03-29
Merge PR #11944: Remove SearchAbout command, deprecated in 8.5
Théo Zimmermann
2020-03-28
Remove SearchAbout command, deprecated in 8.5
Jim Fehrle
2020-03-28
Document change of behavior of Fail in 8.11.
Théo Zimmermann
2020-03-28
coqdoc: Add (* begin details *) and (* end details *)
Thomas Letan
2020-03-28
Update fullGrammar and orderedGrammar following #11877.
Théo Zimmermann
2020-03-28
New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.
Théo Zimmermann
2020-03-27
Fix changelog
Vincent Semeria
2020-03-27
Merge PR #11871: Split documentation of coqdoc on separate page.
Clément Pit-Claudel
2020-03-27
Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...
Vincent Semeria
2020-03-27
Merge PR #11848: Nicer printing for decimal constants
Hugo Herbelin
2020-03-27
Merge PR #11751: Fix #11749: don't warn for hidden files.
Maxime Dénès
2020-03-27
Split coqdoc section out of utility chapter (octopus merge).
Théo Zimmermann
2020-03-27
Move section on coqdoc to new location.
Théo Zimmermann
2020-03-27
Remove the part about coqdoc from the utilities chapter.
Théo Zimmermann
2020-03-27
Prepare split of section about coqdoc.
Théo Zimmermann
2020-03-26
Merge PR #11929: Reintroduce a command that was actually used in another one....
Clément Pit-Claudel
2020-03-26
Reintroduce commands that were actually used. Fix build of PDF manual.
Théo Zimmermann
2020-03-26
Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.
Théo Zimmermann
2020-03-26
Change log
Hugo Herbelin
2020-03-26
CIC is printed in all-caps.
Théo Zimmermann
2020-03-26
Removing deprecated destruct syntax _eqn.
Hugo Herbelin
2020-03-26
Shrink refman-prelude files.
Théo Zimmermann
2020-03-26
Remove outdated mention of -allow-sprop.
Théo Zimmermann
[next]