aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2018-08-02Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' ↵Théo Zimmermann
and 'The Coq commands' of the Reference Manual.
2018-08-02Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ↵Théo Zimmermann
matching' of the Reference Manual.
2018-08-02Merge PR #8144: Improved grammar and spelling for chapters 'Utilities' and ↵Théo Zimmermann
'CoqIDE' of the Reference Manual.
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', ↵Théo Zimmermann
'Omega' and 'Micromega' of the Reference Manual.
2018-08-01Fix broken link.Daniel R. Grayson
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter ↵Zeimer
'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter.
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the ↵Zeimer
Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq ↵Zeimer
commands' of the Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵Zeimer
'Micromega' of the Reference Manual.
2018-08-01Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the ↵Zeimer
Reference Manual.
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', ↵Théo Zimmermann
'Program' and 'ring and field' chapters of the Reference Manual.
2018-08-01Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a titleThéo Zimmermann
2018-07-31Camlp{4 => 5}Jason Gross
2018-07-31Fix doc for no associativityJason Gross
no associative -> no associativity Also remove some 'a's and 'the's and make a note that this is for parsing (There is a difference between left associativity and no associativity for printing)
2018-07-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-30Some trivial fixes to the custom entry documentation.Théo Zimmermann
2018-07-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵Zeimer
and field' chapters of the Reference Manual.
2018-07-29Miscellaneous uniformization of typography in chapter syntax extensions.Hugo Herbelin
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵Hugo Herbelin
messages.
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical ↵Théo Zimmermann
Structures' of the Reference Manual.
2018-07-28Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to ↵Théo Zimmermann
unify" message
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵Zeimer
Reference Manual.
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
We adopt the convention that error messages with a template use the sphinx syntax used in defining syntax rules.
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-24Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], ↵Hugo Herbelin
[N], [nat] and [string]
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
The rule uses s'_j, the text refers to s_j, the latter is simpler in the absence of any other constraints.
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Zeimer
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed ↵Zeimer
the formatting and renamed the tactics to match modern naming conventions.
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Zeimer
Manual.
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
It seems that p is a natural number, so why not write it as 0 rather than the empty list for tree and forest? And, if I understand correctly, odd and even have p = 0 and Arr(even) = Arr(odd) = 1.
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
This trace of V7 syntax remained unnoticed (since July 2004).
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
Including using subscripts more often.
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
2018-07-20Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer
2018-07-20Fixed many spelling and grammar errors in the chapters 'Vernacular ↵Zeimer
commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red.
2018-07-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵Zeimer
of the Reference Manual.
2018-07-19Fixed some typos and grammar errors from section 'The language' of the ↵Zeimer
Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 13:41:37 +0000