aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
* Solved problems with snippets giving errors in chapter 'Detailed examples of ...Gravatar Zeimer2018-07-21
* Rewrote examples about permutations, logic and type isomorphisms: changed the...Gravatar Zeimer2018-07-21
* Improvements for the chapter 'Detailed examples of tactics' of the Reference ...Gravatar Zeimer2018-07-21
* Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' an...Gravatar Théo Zimmermann2018-07-21
|\
* | Small improvements suggested in comments to PR #8086.Gravatar Zeimer2018-07-20
* | Improved chapter 'The tactic language' of the Reference Manual.Gravatar Zeimer2018-07-20
| * Added :undocumented: and :cmd: as suggested in comments for PR #8072.Gravatar Zeimer2018-07-20
| * Fixed many spelling and grammar errors in the chapters 'Vernacular commands',...Gravatar Zeimer2018-07-20
|/
* Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' o...Gravatar Zeimer2018-07-19
* Fixed some typos and grammar errors from section 'The language' of the Refere...Gravatar Zeimer2018-07-19
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
* Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of th...Gravatar Théo Zimmermann2018-07-13
|\
| * Fixed typos, wording and grammar errors in the Preamble of the Reference Manu...Gravatar Zeimer2018-07-12
* | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
|/
* fixed typo for assert_suceedGravatar charguer2018-07-10
* Merge PR #8028: Fix a few typosGravatar Théo Zimmermann2018-07-10
|\
* \ Merge PR #8025: Fix rst syntax for `quote ident {ident}`Gravatar Théo Zimmermann2018-07-10
|\ \
| | * Fix typo in doc/proof-engine/tactics.rst.Gravatar whitequark2018-07-10
| |/ |/|
* | Merge PR #7920: Generic syntax for attributesGravatar Maxime Dénès2018-07-09
|\ \
| | * Fix rst syntax for `quote ident {ident}`Gravatar Joachim Breitner2018-07-09
| |/ |/|
* | Remove Emacs modes.Gravatar Théo Zimmermann2018-07-08
* | Merge PR #7921: Archive the `gallina` toolGravatar Maxime Dénès2018-07-07
|\ \
* | | doc: Fix markup in Calculus of Inductive ConstructionsGravatar Fabian2018-07-04
| | * Describe attributes in the documentation.Gravatar Vincent Laporte2018-07-03
| |/ |/|
* | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \
* \ \ Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \ \
* \ \ \ Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsGravatar Théo Zimmermann2018-07-02
|\ \ \ \
| | | * | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| | * | | Document option Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | |/ /
| * / / doc: typesetting and hyperlinks in Syntax ExtensionsGravatar Lysxia2018-06-30
| |/ /
* / / doc: Fix typesetting in Gallina extensionsGravatar Lysxia2018-06-29
|/ /
* | Self-credit for the work done.Gravatar Théo Zimmermann2018-06-28
* | wrong sphinx syntaxGravatar Ambroise2018-06-28
* | Update gallina-extensions.rstGravatar Ambroise2018-06-28
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
* \ \ Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Gravatar Maxime Dénès2018-06-26
|\ \ \
* \ \ \ Merge PR #7851: Modernize the introduction of the reference manual.Gravatar Maxime Dénès2018-06-26
|\ \ \ \
| | | | * Archive the `gallina` toolGravatar Vincent Laporte2018-06-25
| |_|_|/ |/| | |
* | | | Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \
| | | | * Documenting the syntax of mutual keywords.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|/ |/| | |
* | | | Merge PR #7784: Remove Tutorials from a few other places following #7466.Gravatar Maxime Dénès2018-06-24
|\ \ \ \
* | | | | [ssr] document {}/viewGravatar Enrico Tassi2018-06-22
* | | | | [ssr] document rewrite {}fooGravatar Enrico Tassi2018-06-22
| | | | * Clarify further doc/README.md following Jim's comments.Gravatar Théo Zimmermann2018-06-22
| | | | * Fix copyright dates in doc/LICENSE.Gravatar Théo Zimmermann2018-06-22
| | | | * Improve doc/README.md.Gravatar Théo Zimmermann2018-06-22
| | | | * Move INSTALL.doc into doc/README.md.Gravatar Théo Zimmermann2018-06-22
| |_|_|/ |/| | |
* | | | Merge PR #7770: Move indices on top on the TOC. Closes #7764.Gravatar Maxime Dénès2018-06-21
|\ \ \ \
* \ \ \ \ Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...Gravatar Maxime Dénès2018-06-21
|\ \ \ \ \