aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-05Deprecate 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-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Maxime Dénès
supported scenarios.
2018-03-04Fix 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-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
Noticed by Sigurd Schneider.
2018-02-28Added 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-27Typo in the documentation of the `pattern` tacticJoachim Breitner
2018-02-24Merge PR #6819: Document Arguments extra scopes flagMaxime Dénès
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-22Document Arguments extra scopes flagJasper Hugunin
2018-02-20Doc: add Decimal-related files to index-list.html.templateJason Gross
2018-02-20Documenting use of primitive entry names for restricting syntax in notations.Hugo Herbelin
2018-02-20Extended documentation for notations referring to binders.Hugo Herbelin
Talking about the difference between ident and pattern. Giving examples.
2018-02-20A first step at refreshing and documenting the new feature.Hugo Herbelin
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance ↵Maxime Dénès
information.
2018-02-11Documentation for cumulative inductive variance.Gaëtan Gilbert
2018-02-07mention interactive mode for Fail messagePaul Steckler
2018-01-25document the Fail commandPaul Steckler
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-08Merge PR #6489: Update PNGs; mention async error handling; change query ↵Maxime Dénès
window to query pane in text
2018-01-08Merge PR #6497: Add optimize_heap tactic for #6488Maxime Dénès
2018-01-08Merge PR #6526: Fixing various typos in the Credits chapter.Maxime Dénès
2018-01-05Documentation and CHANGES for bracket with goal selector.Théo Zimmermann
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2018-01-03update PNGs; mention async error handling; change query window to query ↵Paul Steckler
pane; use color descriptions
2017-12-20Merge PR #6377: Removal of the FAQ LaTex document.Maxime Dénès
2017-12-19Fix typo in the refman.Théo Zimmermann
2017-12-18Merge PR #6381: A version of [time] that works on constr evaluationMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Maxime Dénès
Extraction Language command
2017-12-18Removing the FAQ, which has been moved to the GitHub wiki for thisMatt Quinn
repository. Also removing FAQ-related build rules.
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
`ssrnat` is mentioned, but it is not distributed with Coq.
2017-12-15Merge PR #6219: Document undocumented optionsMaxime Dénès
2017-12-14Add documentation for time_constrJason Gross
2017-12-14Add doc+changelog entries for new LtacProf tacticsJason Gross
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Maxime Dénès
same right-hand side.
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-14Document Short Module Printing.Gaëtan Gilbert
2017-12-14Document Rewriting Schemes (quickly).Gaëtan Gilbert
2017-12-14Document Record Elimination Schemes.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 17:51:45 +0000