aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2018-08-31Numeral Notation: some documentation in the refmanPierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
This parsing/printing method for nat should be just as fast as the previous dedicated code. Moreover, we could now parse large literals as nat numbers, by leaving them in a half-abstract form such as (Nat.of_uint 123456). This form is convertible to the closed (S (S (S ...))) form, so it shouldn't be a big deal for compatibility, except for if some Ltac stuff relies on (S ...) to be present after parsing. Of course, forcing the computation of a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-30Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as ↵Théo Zimmermann
error" argument in make
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
"treat errors as warnings" flag (-W) is applied. "1" or undefined includes the flag, other values or undefined omit it. Removed the "-warn-error" parameter to configure. "-profile XXX" will no longer cause these flags to be used.
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-28Merge PR #8334: Fix a casing problem noticed by Lars Dölle on Coq-Club.Clément Pit-Claudel
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-28Add index for focusing braces.Théo Zimmermann
And fix wrong indentation.
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann
2018-08-22[refman] Fixing two nested lemma errors.Théo Zimmermann
2018-08-22[sphinx] Fixing of the beginning of the Tactics chapter.Théo Zimmermann
2018-08-21Trivial Sphinx fix in doc.Théo Zimmermann
2018-08-17Define bullet production token.Théo Zimmermann
2018-08-17Minor Sphinx improvements in the bullet documentation.Théo Zimmermann
And fixing a problem with nested proofs.
2018-08-16Merge PR #8198: Fix broken link.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:50:13 +0000