aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \
* \ \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \ \
| | | * [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| |_|/ |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
| | * Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |/ |/|
* | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \
* \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \
* \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ | | | | | | | | | | | | | | | supported scenarios.
| | | | * [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|/ |/| | | | | | | | | | | Following up on #6791, we remove the option "Intuition Iff Unfolding"
| | | * Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| |_|/ |/| |
| | * Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | | | | | | | | | | Noticed by Sigurd Schneider.
| * | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* / Typo in the documentation of the `pattern` tacticGravatar Joachim Breitner2018-02-27
|/
* Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \
| | * Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |/ |/|
| * Doc: add Decimal-related files to index-list.html.templateGravatar Jason Gross2018-02-20
| |
* | Documenting use of primitive entry names for restricting syntax in notations.Gravatar Hugo Herbelin2018-02-20
| |
* | Extended documentation for notations referring to binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | Talking about the difference between ident and pattern. Giving examples.
* | A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
|/
* Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ | | | | | | information.
| * Documentation for cumulative inductive variance.Gravatar Gaëtan Gilbert2018-02-11
| |
* | mention interactive mode for Fail messageGravatar Paul Steckler2018-02-07
|/
* document the Fail commandGravatar Paul Steckler2018-01-25
|
* Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\
* \ Merge PR #6489: Update PNGs; mention async error handling; change query ↵Gravatar Maxime Dénès2018-01-08
|\ \ | | | | | | | | | window to query pane in text
* \ \ Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\ \ \
* \ \ \ Merge PR #6526: Fixing various typos in the Credits chapter.Gravatar Maxime Dénès2018-01-08
|\ \ \ \
| | | | * Documentation and CHANGES for bracket with goal selector.Gravatar Théo Zimmermann2018-01-05
| |_|_|/ |/| | |
| | * | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
| |/ / |/| |
| | * update PNGs; mention async error handling; change query window to query ↵Gravatar Paul Steckler2018-01-03
| |/ |/| | | | | pane; use color descriptions
* | Merge PR #6377: Removal of the FAQ LaTex document.Gravatar Maxime Dénès2017-12-20
|\ \
* | | Fix typo in the refman.Gravatar Théo Zimmermann2017-12-19
| | |
* | | Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Extraction Language command
| | | | * | Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
| | | | | | | | | | | | | | | | | | | | | | | | repository. Also removing FAQ-related build rules.
* | | | | | [doc] Nit on the manual.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | | | | | | | | | | | | | | | | | | | | | | | `ssrnat` is mentioned, but it is not distributed with Coq.
* | | | | | Merge PR #6219: Document undocumented optionsGravatar Maxime Dénès2017-12-15
|\ \ \ \ \ \
| | | | * | | Add documentation for time_constrGravatar Jason Gross2017-12-14
| | | |/ / /
| | | * / / Add doc+changelog entries for new LtacProf tacticsGravatar Jason Gross2017-12-14
| |_|/ / / |/| | | |
* | | | | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | same right-hand side.
* \ \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | * | | | Document Short Module Printing.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Rewriting Schemes (quickly).Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Record Elimination Schemes.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Asymmetric Patterns.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document some omega options (missing Omega Oldstyle).Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Debug RAKAM.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Debug Cbv.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 07:15:18 +0000