Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6551: Bracket with goal selector | 2018-01-16 | |
|\ | |||
* \ | Merge PR #6489: Update PNGs; mention async error handling; change query ↵ | 2018-01-08 | |
|\ \ | | | | | | | | | | window to query pane in text | ||
* \ \ | Merge PR #6497: Add optimize_heap tactic for #6488 | 2018-01-08 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6526: Fixing various typos in the Credits chapter. | 2018-01-08 | |
|\ \ \ \ | |||
| | | | * | Documentation and CHANGES for bracket with goal selector. | 2018-01-05 | |
| |_|_|/ |/| | | | |||
| | * | | add optimize_heap tactic for #6488 | 2018-01-03 | |
| |/ / |/| | | |||
| | * | update PNGs; mention async error handling; change query window to query ↵ | 2018-01-03 | |
| |/ |/| | | | | | pane; use color descriptions | ||
* | | Merge PR #6377: Removal of the FAQ LaTex document. | 2017-12-20 | |
|\ \ | |||
* | | | 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 | ||
| | | | * | | Removing the FAQ, which has been moved to the GitHub wiki for this | 2017-12-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | repository. Also removing FAQ-related build rules. | ||
* | | | | | | [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 | |
|/ / / | |||
* | | | Merge PR #1033: Universe binder improvements | 2017-11-28 | |
|\ \ \ | |||
* | | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | 2017-11-25 | |
| | | | | |||
| * | | | Allow local universe renaming in Print. | 2017-11-25 | |
|/ / / | |||
| * / | use OCaml criteria for infix ops, #6212 | 2017-11-22 | |
|/ / |