aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
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 windo...Maxime Dénès
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 pane;...Paul Steckler
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 Extra...Maxime Dénès
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
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 sa...Maxime Dénès
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
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
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
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
2017-12-01clarify operation of sequences, #6095Paul Steckler
2017-12-01[refman] Expand a little on global universes.Matthieu Sozeau
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-12-01Merge PR #6276: Coqchk accepts filenamesMaxime Dénès
2017-11-29Documenting the possibility to pass filenames to coqchk.Pierre-Marie Pédrot
2017-11-28use \ocaml macro in new textPaul Steckler
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-22use OCaml criteria for infix ops, #6212Paul Steckler
2017-11-19Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gaëtan Gilbert
2017-11-13coq_makefile: document COQ_SRC_SUBDIRSEnrico Tassi
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:11:15 +0000