index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
language
Age
Commit message (
Expand
)
Author
2020-01-07
Correct manual about implicit parameters in inductives.
SimonBoulier
2020-01-07
Trailing implicit error: documentation
SimonBoulier
2020-01-06
doc: mention limitation of bidi hints vs program
Gaëtan Gilbert
2020-01-06
Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migra...
Clément Pit-Claudel
2019-12-31
Merge PR #11325: [refman] Add missing s.
Pierre-Marie Pédrot
2019-12-29
Remove :flag: that appears in the output
Jim Fehrle
2019-12-29
[refman] Fix bad quoting practice leftover from Sphinx migration.
Théo Zimmermann
2019-12-29
Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...
Théo Zimmermann
2019-12-28
Convert productionlists to prodns
Jim Fehrle
2019-12-28
Update doc/sphinx/language/gallina-extensions.rst
Kazuhiko Sakaguchi
2019-12-28
Extend `Print Canonical Projections` with a search functionality
Kazuhiko Sakaguchi
2019-12-24
[Attributes] accept #[canonical] (Let|Definition)
Enrico Tassi
2019-12-22
[refman] Add missing s.
Théo Zimmermann
2019-12-02
[CS] support #[local] attribute
Enrico Tassi
2019-11-20
Update grammar in the Terms section of Gallina chapter
Jim Fehrle
2019-11-14
Fix doc for universes(foo) attributes
Gaëtan Gilbert
2019-11-08
Merge PR #11050: Replace "option" in doc when it refers to a flag
Théo Zimmermann
2019-11-06
Replace "option" in doc when it refers to a flag
Jim Fehrle
2019-11-04
Cite POPL19 SProp paper
Gaëtan Gilbert
2019-11-01
docs(gallina-extensions.rst): Say more on float literals extraction
Erik Martin-Dorel
2019-11-01
docs: Add refman+stdlib documentation
Erik Martin-Dorel
2019-10-31
Merge PR #10985: Print argument info as an Arguments command in About
Emilio Jesus Gallego Arias
2019-10-31
Merge PR #10997: Implement the unsupported attribute error using the warning ...
Emilio Jesus Gallego Arias
2019-10-31
Doc: index command Arguments with assert
Gaëtan Gilbert
2019-10-30
Implement the unsupported attribute error using the warning system
Gaëtan Gilbert
2019-10-30
Use bullets and indentation (but the result rendering is weird).
Théo Zimmermann
2019-10-30
Use explicit match as suggested by Clément.
Théo Zimmermann
2019-10-30
[refman] Add a second example of contradiction when positivity checking is di...
Théo Zimmermann
2019-10-30
[refman] Give an example of contradiction when positivity checking is disabled.
Théo Zimmermann
2019-10-22
documentation fixes
Antonio Nikishaev
2019-10-06
Fix #10831: minor issues in documentation of Function.
Théo Zimmermann
2019-08-26
Document `Template Check` flag and add changelog entry for 9918
Matthieu Sozeau
2019-08-16
Add documentation for typing flags.
SimonBoulier
2019-08-05
Remove reference to removed option Printing Primitive Projection Compatibility
Jim Fehrle
2019-07-30
Merge PR #10430: [Extraction] Add support for primitive integers
Maxime Dénès
2019-07-28
Update documentation on tokens, use "int" and "num"
Jim Fehrle
2019-07-22
[Int63] Implement all primitives in OCaml
Vincent Laporte
2019-07-22
[Extraction] Add support for primitive integers
Vincent Laporte
2019-06-06
`deprecated` attribute support for notations and syntactic definitions
Maxime Dénès
2019-06-04
[function] always open a proof when used with `wf` or `measure`
Enrico Tassi
2019-05-28
[elaboration] Bidirectionality hints
Maxime Dénès
2019-05-24
Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Emilio Jesus Gallego Arias
2019-05-23
do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Georges Gonthier
2019-05-23
Define many undefined tokens, and other misc fixes.
Théo Zimmermann
2019-05-22
[refman] Give explicit names to the various 'Arguments' commands
Clément Pit-Claudel
2019-05-22
Merge PR #10178: Improve doc for generalizing binders
Théo Zimmermann
2019-05-22
Improve doc for generalizing binders
Gaëtan Gilbert
2019-05-19
[refman] Fix up the grammar entry for field_def
Clément Pit-Claudel
2019-05-19
[refman] Misc fixes (indentation, whitespace, notation syntax)
Clément Pit-Claudel
2019-05-19
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...
Théo Zimmermann
[prev]
[next]