| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-13 | [Sphinx] add bibliography | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Add indexes | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add table of contents | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add doc preamble | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add a few grammar constructions | Maxime Dénès | |
| Code from Paul Steckler (MIT). | |||
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | |
| 2018-03-09 | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | |
| 2018-03-09 | Merge PR #6818: Sphinx doc infrastructure | Maxime Dénès | |
| 2018-03-09 | Moving Gitlab CI documentation build to the main Coq build. | Maxime Dénès | |
| 2018-03-09 | Integration of a sphinx-based documentation generator. | Maxime Dénès | |
| The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content. | |||
| 2018-03-09 | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | |
| 2018-03-09 | doc and changes for coercion from prop/type | charguer | |
| 2018-03-09 | Merge PR #6937: Add empty compat file for Coq 8.8 | Maxime Dénès | |
| 2018-03-08 | [compat] Remove "Refolding Reduction" option. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895. | |||
| 2018-03-08 | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | |
| 2018-03-08 | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | |
| 2018-03-08 | Merge PR #6903: [compat] Remove "Shrink Abstract" | Maxime Dénès | |
| 2018-03-07 | Add empty compat file for Coq 8.8 | Jason Gross | |
| This closes #6598 | |||
| 2018-03-06 | Remove outdated information regarding the FAQ. | Théo Zimmermann | |
| The FAQ is not part of the Coq sources anymore. | |||
| 2018-03-06 | [compat] Remove "Shrink Abstract" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we the option "Shrink Abstract". | |||
| 2018-03-06 | Merge PR #6896: [compat] Remove NOOP deprecated options. | Maxime Dénès | |
| 2018-03-06 | Merge PR #6824: Remove deprecated options related to typeclasses. | Maxime Dénès | |
| 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 #6791: Removing compatibility support for versions older than 8.5. | Maxime Dénès | |
| 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-02 | Remove 8.5 compatibility support. | Théo Zimmermann | |
| 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-24 | Merge PR #6819: Document Arguments extra scopes flag | Maxime Dénès | |
| 2018-02-24 | Merge PR #6599: Decimals in prelude | Maxime Dénès | |
| 2018-02-22 | Document Arguments extra scopes flag | Jasper Hugunin | |
| 2018-02-20 | Doc: add Decimal-related files to index-list.html.template | Jason Gross | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |