| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-25 | [Vernacular] Deprecate the “Show Script” command | Vincent Laporte | |
| Fixes #8320 | |||
| 2019-03-20 | Merge PR #8669: Show diffs in some error messages | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle | |||
| 2019-03-10 | Merge PR #9654: [sphinx] Add warn option to coqtop directive. | Clément Pit-Claudel | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel | |||
| 2019-03-08 | [sphinx] Fix typo in local application of tactics | hawnzug | |
| 2019-03-07 | Merge PR #9133: Move README-V1-V5 to credits chapter | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-02-28 | Show diffs in error messages if color is enabled | Jim Fehrle | |
| 2019-03-01 | [doc] ssr: Fix the documentation of `by [tacs]` | Erik Martin-Dorel | |
| Closes coq/coq#9669 | |||
| 2019-02-28 | Move content of README-V1-V5 to Credits chapter. | Théo Zimmermann | |
| 2019-02-28 | [sphinx] Add warn option to coqtop directive. | Théo Zimmermann | |
| By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected. | |||
| 2019-02-25 | [Manual] Refactor documentation of internal registration commands | Vincent Laporte | |
| 2019-02-25 | [Manual] Document primitive integers | Vincent Laporte | |
| 2019-02-25 | [Manual] Document the “Primitive” command | Vincent Laporte | |
| 2019-02-25 | [Manual] Document “Register Inline” | Vincent Laporte | |
| 2019-02-25 | [Manual] Document “Register” to kernel namespace | Vincent Laporte | |
| 2019-02-19 | [sphinx] Refactor handling of options for coqtop directive. | Théo Zimmermann | |
| Make it mandatory to give exactly one display option. | |||
| 2019-02-18 | Using options abort and restart of coqtop directive in the manual. | Théo Zimmermann | |
| 2019-02-18 | Sphinx: fail when a command fails | Gaëtan Gilbert | |
| This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail). | |||
| 2019-02-18 | Fix last nested lemma failure. | Théo Zimmermann | |
| 2019-02-18 | Merge PR #9142: Disable Ltac backtraces | Hugo Herbelin | |
| Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot | |||
| 2019-02-14 | Merge PR #9571: Document the now_show tactic. | Clément Pit-Claudel | |
| Ack-by: Zimmi48 Reviewed-by: cpitclaudel | |||
| 2019-02-14 | Document the now_show tactic. | Théo Zimmermann | |
| It was used in the standard library and the test-suite but undocumented so far. | |||
| 2019-02-14 | [Manual] Clean examples for `apply` | Vincent Laporte | |
| 2019-02-14 | [Manual] Don’t use `Undo` in ssreflect examples | Vincent Laporte | |
| 2019-02-14 | [Manual] Clean examples about `inversion` tactic | Vincent Laporte | |
| 2019-02-13 | Merge PR #9553: Sphinx various fixing of failing commands | Théo Zimmermann | |
| Ack-by: Zimmi48 | |||
| 2019-02-12 | Fix failing coqtops in tactics.rst | Gaëtan Gilbert | |
| 2019-02-12 | Fix failing coqtops in ssreflect-proof-language.rst | Gaëtan Gilbert | |
| 2019-02-12 | Fix failing coqtops in ltac.rst | Gaëtan Gilbert | |
| 2019-02-12 | Improve the documentation of auto. | Théo Zimmermann | |
| In particular, mention that auto does not use full-blown apply. | |||
| 2019-02-06 | Document the possibility of declaring a Ltac name_goal. | Théo Zimmermann | |
| 2019-02-05 | Documenting the Ltac Backtrace flag. | Pierre-Marie Pédrot | |
| 2019-02-05 | Add advice and an example to the documentation of fold. | Théo Zimmermann | |
| 2019-01-28 | Surround "assumption" with :tacn:`` in tactics.rst | Ryan Scott | |
| 2019-01-28 | Merge PR #9341: [ssr] uniform clear discipline | Maxime Dénès | |
| Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |