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
2019-03-28
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers o...
Maxime Dénès
2019-03-28
Merge PR #9743: Relax the ambiguous path condition of coercion
Enrico Tassi
2019-03-27
Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.
Jim Fehrle
2019-03-27
[doc] [abstract] Document a bit some problems with abstract.
Emilio Jesus Gallego Arias
2019-03-27
[plugin tutorial] Adapt to removal of imperative state.
Emilio Jesus Gallego Arias
2019-03-27
Deprecate `Refine Instance Mode` option
Maxime Dénès
2019-03-26
Merge PR #9829: [Vernacular] Deprecate the “Show Script” command
Enrico Tassi
2019-03-26
Fix syntax of Typeclasses eauto := in reference manual.
Théo Zimmermann
2019-03-25
[Vernacular] Deprecate the “Show Script” command
Vincent Laporte
2019-03-25
Remove `Automatic Coercions Import` option.
Maxime Dénès
2019-03-25
Fix indentation
Gan Shen
2019-03-25
Update doc/sphinx/language/gallina-extensions.rst
Théo Zimmermann
2019-03-24
Fix typo
Gan Shen
2019-03-22
Merge PR #8560: Unicode bindings for CoqIDE that works out of the box
Pierre-Marie Pédrot
2019-03-21
Merge PR #9789: [Manual] Improve documentation on Section, Variable, Context
Théo Zimmermann
2019-03-20
Merge PR #8669: Show diffs in some error messages
Emilio Jesus Gallego Arias
2019-03-18
[Manual] Parametrize -> ParametErize
Lysxia
2019-03-18
Update doc and changes
Kazuhiko Sakaguchi
2019-03-18
[Manual] Move command Context after Let, and more polishing
Lysxia
2019-03-18
fix documentation issues, and add entry to change log
charguer
2019-03-18
polishing documentation for coqide bindings, following @Zimmi48 comments
charguer
2019-03-18
final polishing for coqide bindings
charguer
2019-03-18
documentation for unicode bindings
charguer
2019-03-17
[Manual] Move doc on Let into Section mechanism, and more polishing
Lysxia
2019-03-17
[Manual] Gather section-specific commands in Section documentation (fix #9704)
Lysxia
2019-03-17
[Manual] Improve chapter Type classes, and add mention of Context under Variable
Lysxia
2019-03-14
Documentation for SProp
Gaëtan Gilbert
2019-03-14
Add StrictProp.v with basic SProp related definitions
Gaëtan Gilbert
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-03-13
[refman] Fix Sphinx-translation regression in Arguments command.
Théo Zimmermann
2019-03-13
[refman] Remove warning silencing by fixing the underlying issue.
Théo Zimmermann
2019-03-13
[refman] Fix other newly emitted warnings.
Théo Zimmermann
2019-03-12
[refman] Add 'warn' option to coqtop directive.
Théo Zimmermann
2019-03-12
Merge PR #9389: Implement a method for manual declaration of implicits.
Emilio Jesus Gallego Arias
2019-03-10
Merge PR #9654: [sphinx] Add warn option to coqtop directive.
Clément Pit-Claudel
2019-03-08
[sphinx] Fix typo in local application of tactics
hawnzug
2019-03-07
Merge PR #9133: Move README-V1-V5 to credits chapter
Clément Pit-Claudel
2019-02-28
Show diffs in error messages if color is enabled
Jim Fehrle
2019-03-01
[doc] ssr: Fix the documentation of `by [tacs]`
Erik Martin-Dorel
2019-02-28
Add DOIs.
Théo Zimmermann
2019-02-28
Move content of README-V1-V5 to Credits chapter.
Théo Zimmermann
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2019-02-28
[sphinx] Add warn option to coqtop directive.
Théo Zimmermann
2019-02-28
Merge PR #9578: Document primitive integers
Théo Zimmermann
2019-02-26
[dune] Simple rule to generate Stdlib's documentation.
Emilio Jesus Gallego Arias
2019-02-26
Merge PR #9567: [vernac] Unify declaration hooks.
Maxime Dénès
2019-02-25
[Manual] Refactor documentation of internal registration commands
Vincent Laporte
2019-02-25
[Manual] Document primitive integers
Vincent Laporte
2019-02-25
[Manual] Document the “Primitive” command
Vincent Laporte
2019-02-25
[Manual] Document “Register Inline”
Vincent Laporte
[next]