aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | 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.
* [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | 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.
* 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
| | | | 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
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 09:51:23 +0000