aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge PR #6219: Document undocumented optionsGravatar Maxime Dénès2017-12-15
|\
* \ 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
|\ \
* \ \ 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
|/ /
| * use OCaml criteria for infix ops, #6212Gravatar Paul Steckler2017-11-22
|/
* Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
* coq_makefile: document COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-11-13
* Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Gravatar Samuel Gruetter2017-11-06
* Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\
* \ Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Gravatar Maxime Dénès2017-10-27
|\ \
* | | Rename \Tree to \NatTreeGravatar Johannes Kloos2017-10-25
| | * Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
* | | Fix #5763: Strictly positive example is out of order.Gravatar jkloos2017-10-24
| * | Fix #4846Gravatar Johannes Kloos2017-10-24
| * | Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
| * | Documentation: Add various basic constructs to the index.Gravatar Johannes Kloos2017-10-24
| * | Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
|/ /
* | Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
* | Merge PR #1116: Updating citing Coq in FAQ.Gravatar Maxime Dénès2017-10-10
|\ \ | |/ |/|
| * Updating citing Coq in FAQ.Gravatar Hugo Herbelin2017-10-10
* | Fix copyright info in reference manual.Gravatar Théo Zimmermann2017-10-06
* | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\ \