| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-13 | Merge PR #8616: Include the full Table of Contents document in the on-screen ↵ | Clément Pit-Claudel | |
| TOC, ... | |||
| 2018-10-13 | Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode. | Clément Pit-Claudel | |
| 2018-10-10 | Fix names for 2 entries in Flags, Options, Tables index. | Jim Fehrle | |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-04 | Add missing indexes for Hint Cut and Hint Mode. | Théo Zimmermann | |
| 2018-10-01 | Merge PR #7634: Extend combined scheme to Schemes in Type | Matthieu Sozeau | |
| 2018-10-01 | Merge PR #8301: Documentation for proof diffs | Théo Zimmermann | |
| 2018-09-27 | Merge PR #8475: Centralize the reliance on abstract universe context internals | Gaëtan Gilbert | |
| 2018-09-26 | Combined Scheme tests sort to use either "*" or "/\" | Théo Winterhalter | |
| And update documentation. | |||
| 2018-09-23 | Documentation for proof diffs | Jim Fehrle | |
| 2018-09-21 | Universe binders are Id, not Name. Never print Var. | Gaëtan Gilbert | |
| Comes with minor cleanups in exception catching and unnecessary mapi. | |||
| 2018-09-20 | Rewrite "Flags, Options and Tables" section. | Jim Fehrle | |
| Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: | |||
| 2018-09-20 | [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979 | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-17 | Add missing index entries. | Théo Zimmermann | |
| In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249. | |||
| 2018-09-14 | Merge PR #7894: Remove quote plugin | Théo Zimmermann | |
| 2018-09-12 | Remove quote plugin | Maxime Dénès | |
| As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore. | |||
| 2018-09-12 | Manual: fix documentation of the “fresh” tactic | Vincent Laporte | |
| 2018-09-11 | Grammar entry for the ssr syntax for anonymous arguments. | Assia Mahboubi | |
| 2018-09-06 | Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate. | Pierre-Marie Pédrot | |
| 2018-08-31 | Merge PR #8170: Don't index names starting with `_` in docs | Théo Zimmermann | |
| 2018-08-31 | Fixed the seealso directive in a few places. | Zeimer | |
| 2018-08-31 | Uniformized 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-29 | Merge PR #8353: [sphinx] Fix timeout issue by splitting imports. | Clément Pit-Claudel | |
| 2018-08-29 | Merge 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-28 | Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter. | Clément Pit-Claudel | |
| 2018-08-28 | Add index for focusing braces. | Théo Zimmermann | |
| And fix wrong indentation. | |||
| 2018-08-27 | Document focusing on named goals. | Théo Zimmermann | |
| 2018-08-24 | Merge PR #8266: Minor Sphinx improvements in the bullet documentation. | Clément Pit-Claudel | |
| 2018-08-22 | Fix #8251: remove "the the" occurrences | Gaëtan Gilbert | |
| 2018-08-22 | Add 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-17 | Define bullet production token. | Théo Zimmermann | |
| 2018-08-17 | Minor Sphinx improvements in the bullet documentation. | Théo Zimmermann | |
| And fixing a problem with nested proofs. | |||
| 2018-08-16 | Merge PR #8109: [doc] Fix grammar of goal selectors. | Maxime Dénès | |
| 2018-08-16 | Merge PR #8108: A few Sphinx fixes in the Ltac chapter. | Maxime Dénès | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clément Pit-Claudel | |
| Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines. | |||
| 2018-07-28 | Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵ | Hugo Herbelin | |
| messages. | |||
| 2018-07-26 | [sphinx] Do name cleanup in handle_signature | Clément Pit-Claudel | |
| 2018-07-25 | Doc: preliminary work before #7291 which add an "Unable to unify" message. | Hugo Herbelin | |
| We adopt the convention that error messages with a template use the sphinx syntax used in defining syntax rules. | |||
| 2018-07-24 | Update the documentation w.r.t. the new error raised by unify. | Pierre-Marie Pédrot | |
| 2018-07-21 | Solved problems with snippets giving errors in chapter 'Detailed examples of ↵ | Zeimer | |
| 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. | |||
| 2018-07-21 | Rewrote examples about permutations, logic and type isomorphisms: changed ↵ | Zeimer | |
| the formatting and renamed the tactics to match modern naming conventions. | |||
| 2018-07-21 | Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵ | Zeimer | |
| Manual. | |||
| 2018-07-21 | Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵ | Théo Zimmermann | |
| and 'Tactics' of the Reference Manual. | |||
| 2018-07-21 | Fixing capital letters in the "in" syntax of instantiate. | Hugo Herbelin | |
| This trace of V7 syntax remained unnoticed (since July 2004). | |||
| 2018-07-21 | [doc] Fix grammar of goal selectors. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |