aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2018-08-16Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examplesMaxime Dénès
2018-08-16Merge PR #8109: [doc] Fix grammar of goal selectors.Maxime Dénès
2018-08-16Merge PR #8108: A few Sphinx fixes in the Ltac chapter.Maxime Dénès
2018-08-06Merge PR #8189: Some trivial fixes to the custom entry documentation.Emilio Jesus Gallego Arias
2018-08-04Merge PR #8142: Improved the grammar and spelling of chapter 'Syntax ↵Théo Zimmermann
extensions and interpretation scopes' of the Reference Manual.
2018-08-04Improved the grammar and spelling of chapter 'Syntax extensions and ↵Zeimer
interpretation scopes' of the Reference Manual.
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 23:20:00 +0000