aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Gravatar Maxime Dénès2018-06-21
|\ \ \ \ \ \
| | | | | | * Mention Company-Coq as well.Gravatar Théo Zimmermann2018-06-20
| | | | | | * Add a good reference for Proof-General as suggested by Clément.Gravatar Théo Zimmermann2018-06-20
| | | | | | * Modernize the introduction of the reference manual.Gravatar Théo Zimmermann2018-06-20
| |_|_|_|_|/ |/| | | | |
| | * | | | On cygwin, pass the filename in a format that coqdoc understands.Gravatar Jim Fehrle2018-06-20
* | | | | | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Gravatar Pierre-Marie Pédrot2018-06-19
|\ \ \ \ \ \
| | * | | | | [doc] Rewrite and document the prodn directiveGravatar Clément Pit-Claudel2018-06-19
| | * | | | | [doc] Fix a typo in the ssreflect chapterGravatar Clément Pit-Claudel2018-06-19
| | * | | | | [doc] Fix uncaught duplicate-label errors in the SSReflect chapterGravatar Clément Pit-Claudel2018-06-19
| | * | | | | [doc] Use productionlist instead of prodn in ring.rstGravatar Clément Pit-Claudel2018-06-19
| |/ / / / / |/| | | | |
| * | | | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* | | | | | Fix #7829: Spurious documentation failures.Gravatar Théo Zimmermann2018-06-18
|/ / / / /
* | | | | Merge PR #7848: Fix a typo in documentationGravatar Théo Zimmermann2018-06-17
|\ \ \ \ \
| | | | * | Remove Tutorial from Additional documentation in refman intro.Gravatar Théo Zimmermann2018-06-17
| | | | * | Remove Tutorials from doc/LICENSE following #7466.Gravatar Théo Zimmermann2018-06-17
| |_|_|/ / |/| | | |
| | | * | Add introduction and credits to the TOC.Gravatar Théo Zimmermann2018-06-17