| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-16 | Merge PR #6551: Bracket with goal selector | Maxime Dénès | |
| 2018-01-08 | Merge PR #6489: Update PNGs; mention async error handling; change query ↵ | Maxime Dénès | |
| window to query pane in text | |||
| 2018-01-08 | Merge PR #6497: Add optimize_heap tactic for #6488 | Maxime Dénès | |
| 2018-01-08 | Merge PR #6526: Fixing various typos in the Credits chapter. | Maxime Dénès | |
| 2018-01-05 | Documentation and CHANGES for bracket with goal selector. | Théo Zimmermann | |
| 2018-01-03 | add optimize_heap tactic for #6488 | Paul Steckler | |
| 2018-01-03 | update PNGs; mention async error handling; change query window to query ↵ | Paul Steckler | |
| pane; use color descriptions | |||
| 2017-12-20 | Merge PR #6377: Removal of the FAQ LaTex document. | Maxime Dénès | |
| 2017-12-19 | Fix typo in the refman. | Théo Zimmermann | |
| 2017-12-18 | Merge PR #6381: A version of [time] that works on constr evaluation | Maxime Dénès | |
| 2017-12-18 | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès | |
| 2017-12-18 | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | Maxime Dénès | |
| Extraction Language command | |||
| 2017-12-18 | Removing the FAQ, which has been moved to the GitHub wiki for this | Matt Quinn | |
| repository. Also removing FAQ-related build rules. | |||
| 2017-12-17 | [doc] Nit on the manual. | Emilio Jesus Gallego Arias | |
| `ssrnat` is mentioned, but it is not distributed with Coq. | |||
| 2017-12-15 | Merge PR #6219: Document undocumented options | Maxime Dénès | |
| 2017-12-14 | Add documentation for time_constr | Jason Gross | |
| 2017-12-14 | Add doc+changelog entries for new LtacProf tactics | Jason Gross | |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | Maxime Dénès | |
| same right-hand side. | |||
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | Document Short Module Printing. | Gaëtan Gilbert | |
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert | |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |