aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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 windo...Gravatar Maxime Dénès2018-01-08
|\ \
* \ \ 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 pane;...Gravatar Paul Steckler2018-01-03
| |/ |/|
* | 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 Extra...Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \
| | | | * | Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
* | | | | | [doc] Nit on the manual.Gravatar Emilio Jesus Gallego Arias2017-12-17
* | | | | | 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 sa...Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ 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
| | | * | | | Add doc for Set Info/Debug Auto/Trivial/Eauto.Gravatar Gaëtan Gilbert2017-12-14
| | | * | | | Add optindex for Set Bullet Behavior.Gravatar Gaëtan Gilbert2017-12-14
| | | * | | | Add doc for Set Congruence VerboseGravatar Gaëtan Gilbert2017-12-14
| | | * | | | Fix typo in doc optindex for Typeclass Resolution ...Gravatar Gaëtan Gilbert2017-12-14
| | * | | | | Documenting the new options for printing "match".Gravatar Hugo Herbelin2017-12-12
| * | | | | | Remove deprecated appcontext and corresponding documentation.Gravatar Théo Zimmermann2017-12-11
| |/ / / / /
* | | | | | [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
* | | | | | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
|/ / / / /
* | | | | Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\ \ \ \ \
| | | * | | use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
| |_|/ / / |/| | | |
* | | | | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6300: Clarify operation of sequences, fixes #6095Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | |
| | * | | | | clarify operation of sequences, #6095Gravatar Paul Steckler2017-12-01
| | | * | | | [refman] Expand a little on global universes.Gravatar Matthieu Sozeau2017-12-01
| |_|/ / / / |/| | | | |
| | | * | | Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
* | | | | | Merge PR #6276: Coqchk accepts filenamesGravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ | |_|/ / / / |/| | / / / | | |/ / / | |/| | |
| * | | | Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| | |/ / | |/| |
| | * | use \ocaml macro in new textGravatar Paul Steckler2017-11-28
* | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
|/ / /
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5.Gravatar Hugo Herbelin2017-11-25
| * | | Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
|/ / /