| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-14 | Document Asymmetric Patterns. | Gaëtan Gilbert | |
| 2017-12-14 | Document some omega options (missing Omega Oldstyle). | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert | |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert | |
| 2017-12-14 | Fix typo in doc optindex for Typeclass Resolution ... | Gaëtan Gilbert | |
| 2017-12-12 | Documenting the new options for printing "match". | Hugo Herbelin | |
| Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause. | |||
| 2017-12-11 | Remove deprecated appcontext and corresponding documentation. | Théo Zimmermann | |
| 2017-12-10 | [make] remove unneeded generated file "tolink.ml" | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-12-10 | [build] Remove coqmktop in favor of ocamlfind. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-12-07 | Merge PR #6277: Qualified import in coqchk | Maxime Dénès | |
| 2017-12-05 | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | Paul Steckler | |
| 2017-12-05 | Merge PR #890: Global universe declarations | Maxime Dénès | |
| 2017-12-05 | Merge PR #6300: Clarify operation of sequences, fixes #6095 | Maxime Dénès | |
| 2017-12-05 | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès | |
| 2017-12-01 | clarify operation of sequences, #6095 | Paul Steckler | |
| 2017-12-01 | [refman] Expand a little on global universes. | Matthieu Sozeau | |
| 2017-12-01 | Documenting the -Q flag of coqchk. | Pierre-Marie Pédrot | |
| 2017-12-01 | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès | |
| 2017-11-29 | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot | |
| 2017-11-28 | use \ocaml macro in new text | Paul Steckler | |
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
| 2017-11-25 | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | Hugo Herbelin | |
| 2017-11-25 | Allow local universe renaming in Print. | Gaëtan Gilbert | |
| 2017-11-22 | use OCaml criteria for infix ops, #6212 | Paul Steckler | |
| 2017-11-19 | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | |
| Fixes #4988. | |||
| 2017-11-13 | coq_makefile: document COQ_SRC_SUBDIRS | Enrico Tassi | |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter | |
| not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | |||
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès | |
| 2017-10-27 | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès | |
| 2017-10-25 | Rename \Tree to \NatTree | Johannes Kloos | |
| 2017-10-25 | Put newlines at the end of files. | Gaëtan Gilbert | |
| 2017-10-24 | Fix #5763: Strictly positive example is out of order. | jkloos | |
| I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example. | |||
| 2017-10-24 | Fix #4846 | Johannes Kloos | |
| 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. | |||
| 2017-10-24 | Fix #5413: [unfold ... in] not documented | Johannes Kloos | |
| Made a description of unfold...in and moved the index entry there. | |||
| 2017-10-24 | Documentation: Add various basic constructs to the index. | Johannes Kloos | |
| This was mentioned in #5631 as well. Now, forall, fun and casts have index entries. | |||
| 2017-10-24 | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | |
| As discussed in the bug report, this adds `(...) and `{...} to the index. | |||
| 2017-10-11 | Remove GeoProof support. | Maxime Dénès | |
| Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq). | |||
| 2017-10-10 | Merge PR #1116: Updating citing Coq in FAQ. | Maxime Dénès | |
| 2017-10-10 | Updating citing Coq in FAQ. | Hugo Herbelin | |
| 2017-10-06 | Fix copyright info in reference manual. | Théo Zimmermann | |
| Also simplifies the way it is presented (no need to be overly precise). | |||
| 2017-10-05 | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵ | Maxime Dénès | |
| to escape non-UTF-8 file names) | |||
| 2017-10-03 | Merge PR #1080: Remove some unused parts of the reference manual. | Maxime Dénès | |
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | |
| We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| 2017-09-22 | Remove some unused parts of the reference manual. | Guillaume Melquiond | |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-13 | Reference manual: A few words about the file system constraints for -Q/-R. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |