| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-24 | Merge PR #9384: Improve the note in the beginning of the Ltac chapter. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-01-24 | Merge PR #9269: Move and rewrite intro pattern section | Théo Zimmermann | |
| Ack-by: Zimmi48 Ack-by: anton-trunov Ack-by: jfehrle | |||
| 2019-01-24 | [doc] warn that (automatic) clears can result in errors | Enrico Tassi | |
| 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-23 | Move and rewrite documentation for intro patterns that was under | Jim Fehrle | |
| the intros tactic to its own subsection. Add grammar and examples. | |||
| 2019-01-23 | Fix the information of the level of ; vs ; [ ] | Théo Zimmermann | |
| 2019-01-23 | Improve the note in the beginning of the Ltac chapter. | Théo Zimmermann | |
| In particular, add an example to illustrate the associativity of ; | |||
| 2019-01-22 | Remove unneeded | in productionlists | Jim Fehrle | |
| 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 | ring and field simplify can take no arguments | thery | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |