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-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
[nit] [plugin_tuto] Remove empty function and use new API directly
Emilio Jesus Gallego Arias
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
Update 11909-fix-≡-level.rst
Jason Gross
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
2020-03-26
Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rsts
Théo Zimmermann
2020-03-26
Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sort
Hugo Herbelin
2020-03-26
Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlib
Hugo Herbelin
2020-03-26
Print a warning when parsing non floating-point values.
Pierre Roux
2020-03-25
Doc_grammar: Update cmd:: and tacn:: constructs in .rsts
Jim Fehrle
2020-03-25
Convert Gallina Extensions to use prodn
Jim Fehrle
2020-03-25
Make the level of ≡ in Int63 consistent with =
Jason Gross
2020-03-25
Update changelog
Pierre Roux
2020-03-24
“auto with zarith”: use “lia” rather than “omega”
Vincent Laporte
2020-03-24
Merge PR #11892: [refman] Fix caching, which was broken by the addition of co...
Théo Zimmermann
[prev]
[next]