aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2018-09-07Recover lost snippetMatěj G
This snippet on pattern matching got lost in the process of migrating to Sphynx.
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-08-31Give a proper error message on num-not in functorJason Gross
Numeral Notations are not well-supported inside functors. We now give a proper error message rather than an anomaly when this occurs.
2018-08-31[numeral notations] support aliasesJason Gross
Aliases of global references can now be used in numeral notations
2018-08-31Add periods in response to PR commentsJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
As per https://github.com/coq/coq/pull/8064#discussion_r209875616 I decided to make it a warning because it seems more flexible that way; users to are flipping back and forth between option types and not option types while designing won't have to update their `abstract after` directives to do so, and users who don't want to allow this can make it an actual error message.
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
Also make `Check S` no longer anomaly Add a couple more test cases for numeral notations Also add another possibly-confusing error message to the doc. Respond to Hugo's doc request with Zimmi48's suggestion From https://github.com/coq/coq/pull/8064/files#r204191608
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly).
2018-08-31Numeral Notation: minor text improvements suggested by J. GrossPierre Letouzey
2018-08-31Numeral Notation: some documentation in the refmanPierre Letouzey
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-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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 21:48:33 +0000