| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-21 | Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵ | Théo Zimmermann | |
| and 'Tactics' of the Reference Manual. | |||
| 2018-07-20 | Small improvements suggested in comments to PR #8086. | Zeimer | |
| 2018-07-20 | Improved chapter 'The tactic language' of the Reference Manual. | Zeimer | |
| 2018-07-20 | Added :undocumented: and :cmd: as suggested in comments for PR #8072. | Zeimer | |
| 2018-07-20 | Fixed 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-19 | Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵ | Zeimer | |
| of the Reference Manual. | |||
| 2018-07-19 | Fixed 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-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-13 | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵ | Théo Zimmermann | |
| the Reference Manual (Introduction, Credits). | |||
| 2018-07-12 | Fixed typos, wording and grammar errors in the Preamble of the Reference ↵ | Zeimer | |
| Manual (Introduction, Credits). | |||
| 2018-07-12 | Tactic deprecation machinery | Maxime 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-10 | fixed typo for assert_suceed | charguer | |
| 2018-07-10 | Merge PR #8028: Fix a few typos | Théo Zimmermann | |
| 2018-07-10 | Merge PR #8025: Fix rst syntax for `quote ident {ident}` | Théo Zimmermann | |
| 2018-07-10 | Fix typo in doc/proof-engine/tactics.rst. | whitequark | |
| 2018-07-09 | Merge PR #7920: Generic syntax for attributes | Maxime Dénès | |
| 2018-07-09 | Fix rst syntax for `quote ident {ident}` | Joachim Breitner | |
| 2018-07-08 | Remove Emacs modes. | Théo Zimmermann | |
| They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead. | |||
| 2018-07-07 | Merge PR #7921: Archive the `gallina` tool | Maxime Dénès | |
| 2018-07-04 | doc: Fix markup in Calculus of Inductive Constructions | Fabian | |
| 2018-07-03 | Describe attributes in the documentation. | Vincent Laporte | |
| 2018-07-03 | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | Pierre-Marie Pédrot | |
| 2018-07-02 | Merge PR #7703: Add an option to force parameters to be uniform | Matthieu Sozeau | |
| 2018-07-02 | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | Théo Zimmermann | |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu 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-01 | Document option Uniform Inductive Parameters | Jasper Hugunin | |
| 2018-06-30 | doc: typesetting and hyperlinks in Syntax Extensions | Lysxia | |
| 2018-06-29 | doc: Fix typesetting in Gallina extensions | Lysxia | |
| 2018-06-28 | Self-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-28 | wrong sphinx syntax | Ambroise | |
| 2018-06-28 | Update gallina-extensions.rst | Ambroise | |
| I knew this feature existed but I did not remember the syntax and I could not find it in the manual | |||
| 2018-06-28 | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | |
| 2018-06-26 | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | Maxime Dénès | |
| 2018-06-26 | Merge PR #7851: Modernize the introduction of the reference manual. | Maxime Dénès | |
| 2018-06-25 | Archive the `gallina` tool | Vincent Laporte | |
| 2018-06-25 | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | |
| 2018-06-24 | Documenting the syntax of mutual keywords. | Pierre-Marie Pédrot | |
| 2018-06-24 | Merge PR #7784: Remove Tutorials from a few other places following #7466. | Maxime Dénès | |
| 2018-06-22 | [ssr] document {}/view | Enrico Tassi | |
| 2018-06-22 | [ssr] document rewrite {}foo | Enrico Tassi | |
| It was used in some examples, but never fully documented | |||
| 2018-06-22 | Clarify further doc/README.md following Jim's comments. | Théo Zimmermann | |
| Relative links. Cf. #7800. | |||
| 2018-06-22 | Fix copyright dates in doc/LICENSE. | Théo Zimmermann | |
| [ci skip] | |||
| 2018-06-22 | Improve doc/README.md. | Théo Zimmermann | |
| - Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip] | |||
| 2018-06-22 | Move INSTALL.doc into doc/README.md. | Théo Zimmermann | |
| This will avoid in particular this ambiguous file extension. [ci skip] | |||
| 2018-06-21 | Merge PR #7770: Move indices on top on the TOC. Closes #7764. | Maxime Dénès | |
| 2018-06-21 | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵ | Maxime Dénès | |
| understands. | |||
| 2018-06-21 | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | Maxime Dénès | |
| 2018-06-20 | Mention 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-20 | Add a good reference for Proof-General as suggested by Clément. | Théo Zimmermann | |
| 2018-06-20 | Modernize the introduction of the reference manual. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |