| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-24 | [doc] more precise description of when automatic clears are triggered | Enrico Tassi | |
| 2019-01-24 | [doc] explain how to avoid automatic clears | Enrico Tassi | |
| 2019-01-22 | clarify when an ident is added to the clear switch | Enrico Tassi | |
| 2019-01-22 | Apply suggestions from code review | Théo Zimmermann | |
| Co-Authored-By: gares <gares@fettunta.org> | |||
| 2019-01-21 | [ssr] better structure the ipats doc | Enrico Tassi | |
| 2019-01-19 | [ssr] compile "=> {x..} y" as "=> {x..y} y" | Enrico Tassi | |
| This is for consistency with "rewrite {x..} y" | |||
| 2019-01-18 | [ssr] compile "=> {} y" as "=> {y} y" | Enrico Tassi | |
| 2018-12-19 | [doc] typo | Enrico Tassi | |
| 2018-12-18 | [ssr] make > a stand alone intro pattern | Enrico Tassi | |
| 2018-12-18 | [ssr] extended intro patterns: + > [^] /ltac: | Enrico Tassi | |
| This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim). | |||
| 2018-12-14 | Fix the SSReflect chapter regarding objects without bodies. | Théo Zimmermann | |
| 2018-12-11 | Add missing formatting. | Théo Zimmermann | |
| 2018-12-11 | Document the deprecation of hint declaration withou database in refman. | Théo Zimmermann | |
| Follow-up of #8987. | |||
| 2018-12-04 | Add undocumented options from mattam82 | Jim Fehrle | |
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-11-18 | [options] Remove deprecated option automatic introduction. | Emilio Jesus Gallego Arias | |
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-06 | Improve rendering of the credits. | Guillaume Melquiond | |
| This mostly fixes text that was italicized instead of teletyped. When possible, tactic names have been made to point to their documentation. Also, the date of the 8.9 release has been proactively changed to November. | |||
| 2018-10-24 | [Manual] Prevent an irrelevant warning to show up | Vincent Laporte | |
| 2018-10-24 | [Manual] Avoid using deprecated “Focus” | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix rendering of an example | Vincent Laporte | |
| 2018-10-24 | [Manual] Typo | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix an example | Vincent Laporte | |
| The `Undo` command is not reliable. | |||
| 2018-10-24 | [Manual] Fix layout of a list | Vincent Laporte | |
| 2018-10-23 | Fix formatting. Use standard if..then grammar. | Sam Pablo Kuper | |
| 2018-10-15 | Correct some spelling errors | Benjamin Barenblat | |
| 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`. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |