Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix typo in the refman. | 2017-12-19 | |
| | |||
* | Merge PR #6381: A version of [time] that works on constr evaluation | 2017-12-18 | |
|\ | |||
* \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | |
|\ \ | |||
* \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | 2017-12-18 | |
|\ \ \ | | | | | | | | | | | | | Extraction Language command | ||
* | | | | [doc] Nit on the manual. | 2017-12-17 | |
| | | | | | | | | | | | | | | | | `ssrnat` is mentioned, but it is not distributed with Coq. | ||
* | | | | Merge PR #6219: Document undocumented options | 2017-12-15 | |
|\ \ \ \ | |||
| | | | * | Add documentation for time_constr | 2017-12-14 | |
| | | |/ | |||
| | | * | Add doc+changelog entries for new LtacProf tactics | 2017-12-14 | |
| |_|/ |/| | | |||
* | | | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | 2017-12-14 | |
|\ \ \ | | | | | | | | | | | | | same right-hand side. | ||
* \ \ \ | Merge PR #6169: Clean up/deprecated options | 2017-12-14 | |
|\ \ \ \ | |||
| | | * | | Document Short Module Printing. | 2017-12-14 | |
| | | | | | |||
| | | * | | Document Rewriting Schemes (quickly). | 2017-12-14 | |
| | | | | | |||
| | | * | | Document Record Elimination Schemes. | 2017-12-14 | |
| | | | | | |||
| | | * | | Document Asymmetric Patterns. | 2017-12-14 | |
| | | | | | |||
| | | * | | Document some omega options (missing Omega Oldstyle). | 2017-12-14 | |
| | | | | | |||
| | | * | | Add doc for Set Debug RAKAM. | 2017-12-14 | |
| | | | | | |||
| | | * | | Add doc for Set Debug Cbv. | 2017-12-14 | |
| | | | | | |||
| | | * | | Add doc for Set Info/Debug Auto/Trivial/Eauto. | 2017-12-14 | |
| | | | | | |||
| | | * | | Add optindex for Set Bullet Behavior. | 2017-12-14 | |
| | | | | | |||
| | | * | | Add doc for Set Congruence Verbose | 2017-12-14 | |
| | | | | | |||
| | | * | | Fix typo in doc optindex for Typeclass Resolution ... | 2017-12-14 | |
| | | | | | |||
| | * | | | Documenting the new options for printing "match". | 2017-12-12 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause. | ||
| * | | | | Remove deprecated appcontext and corresponding documentation. | 2017-12-11 | |
| |/ / / | |||
* | | | | [make] remove unneeded generated file "tolink.ml" | 2017-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. | 2017-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 coqchk | 2017-12-07 | |
|\ \ \ | |||
| | | * | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | 2017-12-05 | |
| |_|/ |/| | | |||
* | | | Merge PR #890: Global universe declarations | 2017-12-05 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6300: Clarify operation of sequences, fixes #6095 | 2017-12-05 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | 2017-12-05 | |
|\ \ \ \ \ | |||
| | * | | | | clarify operation of sequences, #6095 | 2017-12-01 | |
| | | | | | | |||
| | | * | | | [refman] Expand a little on global universes. | 2017-12-01 | |
| |_|/ / / |/| | | | | |||
| | | * | | Documenting the -Q flag of coqchk. | 2017-12-01 | |
| | | | | | |||
* | | | | | Merge PR #6276: Coqchk accepts filenames | 2017-12-01 | |
|\ \ \ \ \ | |_|/ / / |/| | / / | | |/ / | |/| | | |||
| * | | | Documenting the possibility to pass filenames to coqchk. | 2017-11-29 | |
| | |/ | |/| | |||
| | * | use \ocaml macro in new text | 2017-11-28 | |
| | | | |||
* | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | 2017-11-28 | |
|/ / | |||
* | | Allow local universe renaming in Print. | 2017-11-25 | |
| | | |||
| * | use OCaml criteria for infix ops, #6212 | 2017-11-22 | |
|/ | |||
* | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | 2017-11-19 | |
| | | | | Fixes #4988. | ||
* | coq_makefile: document COQ_SRC_SUBDIRS | 2017-11-13 | |
| | |||
* | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | 2017-11-06 | |
| | | | | | | not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | ||
* | Merge PR #1139: Add a linter. | 2017-11-06 | |
|\ | |||
* \ | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | 2017-10-27 | |
|\ \ | |||
* | | | Rename \Tree to \NatTree | 2017-10-25 | |
| | | | |||
| | * | Put newlines at the end of files. | 2017-10-25 | |
| | | | |||
* | | | Fix #5763: Strictly positive example is out of order. | 2017-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 #4846 | 2017-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 documented | 2017-10-24 | |
| | | | | | | | | | | | | Made a description of unfold...in and moved the index entry there. | ||
| * | | Documentation: Add various basic constructs to the index. | 2017-10-24 | |
| | | | | | | | | | | | | | | | This was mentioned in #5631 as well. Now, forall, fun and casts have index entries. |