| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-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 | |
| 2017-09-11 | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | |
| 2017-09-11 | Merge PR #1035: Fix the introduction of SSR refman chapter. | Maxime Dénès | |
| 2017-09-11 | Merge PR #1014: Add option index entry for NativeCompute Profiling | Maxime Dénès | |
| 2017-09-11 | Merge PR #1004: Document primitive projections in more detail | Maxime Dénès | |
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-09-08 | Fix the introduction of SSR refman chapter. | Théo Zimmermann | |
| 2017-09-03 | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | |
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler | |
| 2017-09-01 | Fixing various typos in the Credits chapter. | Théo Zimmermann | |
| 2017-08-31 | Document primitive projections in more detail | Matthieu Sozeau | |
| 2017-08-31 | RefMan-ssr: fix warning | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #993: Credits for version 8.7 | Maxime Dénès | |
| 2017-08-31 | Credits for version 8.7 | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |