| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-06 | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | Maxime Dénès | |
| 2018-03-05 | Deprecate Focus and Unfocus. | Théo Zimmermann | |
| 2018-03-04 | [compat] Remove NOOP and alias deprecated options. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP. | |||
| 2018-03-04 | Remove deprecated options related to typeclasses. | Théo Zimmermann | |
| 2018-03-04 | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | |
| 2018-03-04 | Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵ | Maxime Dénès | |
| supported scenarios. | |||
| 2018-03-04 | Fix typos. | Théo Zimmermann | |
| 2018-03-03 | [compat] Remove "Intuition Iff Unfolding" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Intuition Iff Unfolding" | |||
| 2018-03-01 | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | |
| Noticed by Sigurd Schneider. | |||
| 2018-02-28 | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin | |
| 2018-02-28 | [toplevel] [vernac] Remove Load hack and check supported scenarios. | Emilio Jesus Gallego Arias | |
| Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now. | |||
| 2018-02-27 | Typo in the documentation of the `pattern` tactic | Joachim Breitner | |
| 2018-02-22 | Document Arguments extra scopes flag | Jasper Hugunin | |
| 2018-02-20 | Documenting use of primitive entry names for restricting syntax in notations. | Hugo Herbelin | |
| 2018-02-20 | Extended documentation for notations referring to binders. | Hugo Herbelin | |
| Talking about the difference between ident and pattern. Giving examples. | |||
| 2018-02-20 | A first step at refreshing and documenting the new feature. | Hugo Herbelin | |
| 2018-02-17 | Implement name mangling option | Jasper Hugunin | |
| 2018-02-12 | Merge PR #6128: Simplification: cumulativity information is variance ↵ | Maxime Dénès | |
| information. | |||
| 2018-02-11 | Documentation for cumulative inductive variance. | Gaëtan Gilbert | |
| 2018-02-07 | mention interactive mode for Fail message | Paul Steckler | |
| 2018-01-25 | document the Fail command | Paul Steckler | |
| 2018-01-16 | Merge PR #6551: Bracket with goal selector | Maxime Dénès | |
| 2018-01-08 | Merge PR #6489: Update PNGs; mention async error handling; change query ↵ | Maxime Dénès | |
| window to query pane in text | |||
| 2018-01-08 | Merge PR #6497: Add optimize_heap tactic for #6488 | Maxime Dénès | |
| 2018-01-08 | Merge PR #6526: Fixing various typos in the Credits chapter. | Maxime Dénès | |
| 2018-01-05 | Documentation and CHANGES for bracket with goal selector. | Théo Zimmermann | |
| 2018-01-03 | add optimize_heap tactic for #6488 | Paul Steckler | |
| 2018-01-03 | update PNGs; mention async error handling; change query window to query ↵ | Paul Steckler | |
| pane; use color descriptions | |||
| 2017-12-19 | Fix typo in the refman. | Théo Zimmermann | |
| 2017-12-18 | Merge PR #6381: A version of [time] that works on constr evaluation | Maxime Dénès | |
| 2017-12-18 | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès | |
| 2017-12-18 | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | Maxime Dénès | |
| Extraction Language command | |||
| 2017-12-17 | [doc] Nit on the manual. | Emilio Jesus Gallego Arias | |
| `ssrnat` is mentioned, but it is not distributed with Coq. | |||
| 2017-12-15 | Merge PR #6219: Document undocumented options | Maxime Dénès | |
| 2017-12-14 | Add documentation for time_constr | Jason Gross | |
| 2017-12-14 | Add doc+changelog entries for new LtacProf tactics | Jason Gross | |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | Maxime Dénès | |
| same right-hand side. | |||
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | Document Short Module Printing. | Gaëtan Gilbert | |
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert | |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert | |
| 2017-12-14 | Document Asymmetric Patterns. | Gaëtan Gilbert | |
| 2017-12-14 | Document some omega options (missing Omega Oldstyle). | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert | |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert | |
| 2017-12-14 | Fix typo in doc optindex for Typeclass Resolution ... | Gaëtan Gilbert | |
| 2017-12-12 | Documenting the new options for printing "match". | Hugo Herbelin | |
| Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |