aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Collapse)Author
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-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
Noticed by Sigurd Schneider.
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-22Document Arguments extra scopes flagJasper Hugunin
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-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-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-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
2017-12-14Document Asymmetric Patterns.Gaëtan Gilbert
2017-12-14Document some omega options (missing Omega Oldstyle).Gaëtan Gilbert
2017-12-14Add doc for Set Debug RAKAM.Gaëtan Gilbert
2017-12-14Add doc for Set Debug Cbv.Gaëtan Gilbert
2017-12-14Add doc for Set Info/Debug Auto/Trivial/Eauto.Gaëtan Gilbert
2017-12-14Add optindex for Set Bullet Behavior.Gaëtan Gilbert
2017-12-14Add doc for Set Congruence VerboseGaëtan Gilbert
2017-12-14Fix typo in doc optindex for Typeclass Resolution ...Gaëtan Gilbert
2017-12-12Documenting the new options for printing "match".Hugo Herbelin
Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause.
2017-12-11Remove deprecated appcontext and corresponding documentation.Théo Zimmermann
2017-12-10[make] remove unneeded generated file "tolink.ml"Emilio Jesus Gallego Arias
When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6300: Clarify operation of sequences, fixes #6095Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 22:22:59 +0000