aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Gravatar Zeimer2018-07-21
| | | | 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.
* Rewrote examples about permutations, logic and type isomorphisms: changed ↵Gravatar Zeimer2018-07-21
| | | | the formatting and renamed the tactics to match modern naming conventions.
* Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Gravatar Zeimer2018-07-21
| | | | Manual.
* Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Gravatar Théo Zimmermann2018-07-21
|\ | | | | | | and 'Tactics' of the Reference Manual.
* | Small improvements suggested in comments to PR #8086.Gravatar Zeimer2018-07-20
| |
* | Improved chapter 'The tactic language' of the Reference Manual.Gravatar Zeimer2018-07-20
| |
| * Added :undocumented: and :cmd: as suggested in comments for PR #8072.Gravatar Zeimer2018-07-20
| |
| * Fixed many spelling and grammar errors in the chapters 'Vernacular ↵Gravatar Zeimer2018-07-20
|/ | | | | | | 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.
* Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵Gravatar Zeimer2018-07-19
| | | | of the Reference Manual.
* Fixed some typos and grammar errors from section 'The language' of the ↵Gravatar Zeimer2018-07-19
| | | | 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.
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
| | | | As stated in the manual, the fourier tactic is subsumed by lra.
* Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵Gravatar Théo Zimmermann2018-07-13
|\ | | | | | | the Reference Manual (Introduction, Credits).
| * Fixed typos, wording and grammar errors in the Preamble of the Reference ↵Gravatar Zeimer2018-07-12
| | | | | | | | Manual (Introduction, Credits).
* | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
* fixed typo for assert_suceedGravatar charguer2018-07-10
|
* 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
| | | | | | | | | | They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
* | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
| | * | | 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
| | | | | | | | | | | | I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
* | wrong sphinx syntaxGravatar Ambroise2018-06-28
| |
* | Update gallina-extensions.rstGravatar Ambroise2018-06-28
| | | | | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
* \ \ 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
| | | | | | | | | | | | | | | | It was used in some examples, but never fully documented
* | | | Merge PR #7770: Move indices on top on the TOC. Closes #7764.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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page.
| | | | | * 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
| |_|_|_|/ |/| | | |
* | | | | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.