aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* 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
| |
* | 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
|/
* Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
| | | | Fixes #4988.
* coq_makefile: document COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-11-13
|
* Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Gravatar Samuel Gruetter2017-11-06
| | | | | | not "first [ progress tac1 | progress tac2 ]". And add a missing backslash.
* 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
| | | | | | | | | | | | | | | | | | I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example.
| * | Fix #4846Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | Bug description: The "now" tactic, which is being used in the standard library, is not documented in the Reference Manual This commit documents the easy tactic, and gives now as a variant.
| * | Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | Made a description of unfold...in and moved the index entry there.
| * | Documentation: Add various basic constructs to the index.Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | This was mentioned in #5631 as well. Now, forall, fun and casts have index entries.
| * | Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
|/ / | | | | | | | | As discussed in the bug report, this adds `(...) and `{...} to the index.
* | Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| | | | | | | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* | 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
| | | | | | | | Also simplifies the way it is presented (no need to be overly precise).
* | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ \ | | | | | | | | | to escape non-UTF-8 file names)
* \ \ Merge PR #1080: Remove some unused parts of the reference manual.Gravatar Maxime Dénès2017-10-03
|\ \ \
* | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|/ |/| | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| * | Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
| | |
* | | Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
|/ /
| * Reference manual: A few words about the file system constraints for -Q/-R.Gravatar Hugo Herbelin2017-09-13
|/
* Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\
* \ Merge PR #1035: Fix the introduction of SSR refman chapter.Gravatar Maxime Dénès2017-09-11
|\ \
* \ \ Merge PR #1014: Add option index entry for NativeCompute ProfilingGravatar Maxime Dénès2017-09-11
|\ \ \
* \ \ \ Merge PR #1004: Document primitive projections in more detailGravatar Maxime Dénès2017-09-11
|\ \ \ \
| | | | * Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
| |_|_|/ |/| | |
| | | * Fix the introduction of SSR refman chapter.Gravatar Théo Zimmermann2017-09-08
| |_|/ |/| |
* | | 2 Typos in 'Add Parametric Morphism' DocumentationGravatar staffehn2017-09-03
| | |
| | * add option index entry for NativeCompute ProfilingGravatar Paul Steckler2017-09-01
| |/ |/|
| * Document primitive projections in more detailGravatar Matthieu Sozeau2017-08-31
| |
| * RefMan-ssr: fix warningGravatar Matthieu Sozeau2017-08-31
| |
* | Merge PR #993: Credits for version 8.7Gravatar Maxime Dénès2017-08-31
|\ \
| * | Credits for version 8.7Gravatar Matthieu Sozeau2017-08-31
| | |
* | | Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \ | |_|/ |/| |
| * | coq_makefile: improve documentationGravatar Enrico Tassi2017-08-29
| | |
* | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \
* \ \ \ Merge PR #988: Fix obsolete description of real numerals.Gravatar Maxime Dénès2017-08-29
|\ \ \ \
* \ \ \ \ Merge PR #819: Cleanup old thingsGravatar Maxime Dénès2017-08-29
|\ \ \ \ \
* \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | | | * Update coypright dates on documentationGravatar Matthieu Sozeau2017-08-23
| |_|_|_|/ |/| | | |
| | | * | Fix obsolete description of real numerals.Gravatar Guillaume Melquiond2017-08-22
| |_|/ / |/| | |
| | | * use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
| | | |
* | | | Merge PR #973: Adding documentation for Printing Focused option.Gravatar Maxime Dénès2017-08-18
|\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 19:29:34 +0000