aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
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.
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-13Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵Théo Zimmermann
the Reference Manual (Introduction, Credits).
2018-07-12Fixed typos, wording and grammar errors in the Preamble of the Reference ↵Zeimer
Manual (Introduction, Credits).
2018-07-12Tactic deprecation machineryMaxime Dénès
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.".
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Merge PR #8025: Fix rst syntax for `quote ident {ident}`Théo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-08Remove Emacs modes.Théo Zimmermann
They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
2018-07-07Merge PR #7921: Archive the `gallina` toolMaxime Dénès
2018-07-04doc: Fix markup in Calculus of Inductive ConstructionsFabian
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
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
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-29doc: Fix typesetting in Gallina extensionsLysxia
2018-06-28Self-credit for the work done.Théo Zimmermann
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.
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Update gallina-extensions.rstAmbroise
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-26Merge PR #7851: Modernize the introduction of the reference manual.Maxime Dénès
2018-06-25Archive the `gallina` toolVincent Laporte
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-24Documenting the syntax of mutual keywords.Pierre-Marie Pédrot
2018-06-24Merge PR #7784: Remove Tutorials from a few other places following #7466.Maxime Dénès
2018-06-22[ssr] document {}/viewEnrico Tassi
2018-06-22[ssr] document rewrite {}fooEnrico Tassi
It was used in some examples, but never fully documented
2018-06-21Merge PR #7770: Move indices on top on the TOC. Closes #7764.Maxime Dénès
2018-06-21Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Maxime Dénès
2018-06-20Mention Company-Coq as well.Théo Zimmermann
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.
2018-06-20Add a good reference for Proof-General as suggested by Clément.Théo Zimmermann
2018-06-20Modernize the introduction of the reference manual.Théo Zimmermann
2018-06-19Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Pierre-Marie Pédrot
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
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.
2018-06-19[doc] Fix a typo in the ssreflect chapterClément Pit-Claudel
2018-06-19[doc] Fix uncaught duplicate-label errors in the SSReflect chapterClément Pit-Claudel
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
2018-06-18Fix #7829: Spurious documentation failures.Théo Zimmermann
We split a Require Import in two to avoid reaching the timeout.
2018-06-17Merge PR #7848: Fix a typo in documentationThéo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 21:04:47 +0000