| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-20 | Rewrite "Flags, Options and Tables" section. | Jim Fehrle | |
| Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: | |||
| 2018-09-21 | [dune] [configure] Allow to set prefix using environment variable. | Emilio Jesus Gallego Arias | |
| This is a hack to enable correct OPAM building, the medium-term plan is to avoid having to set a prefix at configure time but instead using a set of rules to locate the Coq library. We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2 | |||
| 2018-09-21 | Merge PR #8518: [dune] Add "watch" target for continuous build mode. | Théo Zimmermann | |
| 2018-09-20 | [dune] Add "watch" target for continuous build mode. | Emilio Jesus Gallego Arias | |
| `make -f Makefile.dune watch` will now watch for files changes and rebuild what is needed. This feature requires `fswatch` or `inotifywait`, and Dune >= 1.2.0. Note that the current CI image ships an older Dune version. | |||
| 2018-09-20 | Define flags (binary-valued settings) and tables (settings that are sets) | Jim Fehrle | |
| as separate NotationObject types, include in index. | |||
| 2018-09-20 | CHANGES for 8.8.2. | Théo Zimmermann | |
| 2018-09-20 | Current diff code only compares the first current goal of the old and new | Jim Fehrle | |
| proof states. That's not always correct. This change will a) show diffs for all displayed goals and b) correctly match goals between the old and new proof states. For example, "split." will show diffs for both resulting goals. "all: swap 1 2" will show the same diffs as for the old proof state, though in a different position in the output. Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals for a description of how goals are matched between old and new proofs. | |||
| 2018-09-20 | Use "rm -rf" so .coq-native directories are removed. Fixes #8496. | Jim Fehrle | |
| 2018-09-20 | [opam] Fix typo in build variable. | Emilio Jesus Gallego Arias | |
| Fixes #8431 | |||
| 2018-09-20 | Merge PR #8418: Add a PDF version of the manual | Théo Zimmermann | |
| 2018-09-20 | Merge PR #8297: Fix #7754: universe declarations on mutual inductives | Matthieu Sozeau | |
| 2018-09-20 | Stop building LaTeX doc in Travis (keep HTML). | Théo Zimmermann | |
| The LaTeX doc is already tested in GitLab CI and finding the right dependencies in this older version of Ubuntu is a hurdle. | |||
| 2018-09-20 | Mention PDF doc in CHANGES. | Théo Zimmermann | |
| 2018-09-20 | Fix race condition. | Théo Zimmermann | |
| 2018-09-20 | Update minimum required dependency versions of Sphinx doc. | Théo Zimmermann | |
| The minimum required versions of the Sphinx-related (and ANTLR) Python packages for Coq 8.10 were chosen as the lower bound between what is currently in Debian Buster and in NixOS 18.09 Jellyfish (in practice the lower bound was always met by NixOS 18.09 Jellyfish). These minimum required versions were documented. In the docker image used by GitLab CI, we install these Python packages through pip as this allows us to pin them to these specific versions. In Travis, we let them unspecified to always test the latest versions. Finally, we also add the new dependencies of the Sphinx PDF manual. | |||
| 2018-09-20 | [doc] Replace app.info (deprecated in Sphinx 8.0) with logger.info | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Remove unneeded backslashes in biblio.bib | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Skip unneeded copies in copy_formatspecific_files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Move a citation back into the introduction | Clément Pit-Claudel | |
| Alternatively, we could duplicate the citation text in both index files. | |||
| 2018-09-20 | [doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targets | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Remove frames around code snippets in the LateX build | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Change the name that appears on the first page of the PDF manual | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix some Sphinx LaTeX warnings and silence others | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Add another common mistake to the documentation-writing guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a few syntax highlighting issues | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Get rid of two Sphinx warnings | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix more duplicate-label issues in production lists | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Rewrite and document the prodn directive | Clément Pit-Claudel | |
| It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. | |||
| 2018-09-20 | [doc] Add more common mistakes to the documentation-writing guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Mark the dummy index files as orphans (the LaTeX build skips them) | Clément Pit-Claudel | |
| Do we really need these? Wouldn't it be better to just add appropriate links to the html template? | |||
| 2018-09-20 | [doc] Add a warning about overusing the `coqtop` directive | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979 | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Ensure that merging coqtop blocks preserves anchors | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980 | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a typo in the developer guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Improve rendering of Coq objects in PDF output | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Add env_version to metadata of coqrst plugin | Clément Pit-Claudel | |
| This is required by Sphinx 8.0. See https://github.com/sphinx-doc/sphinx/issues/4460. | |||
| 2018-09-20 | [doc] Fix a few LaTeX mistakes | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Create a wrapper around the Credits file for the LaTeX build | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Create a separate zebibliography file for the LaTeX build | Clément Pit-Claudel | |
| `.. bibliography::` puts the bibliography on its own page with its own title in LaTeX, but includes it inline without a title in HTML [1], so we need to maintain two separate copies of zebibliography.rst [1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends | |||
| 2018-09-20 | [doc] Create a separate index file for the LaTeX build | Clément Pit-Claudel | |
| See https://github.com/sphinx-doc/sphinx/issues/4977 for context. | |||
| 2018-09-20 | [doc] Remove an empty '.. bibliography::' in addendum/program | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Explain why zebibliography needs to be separate and oddly-named | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Adjust conf.py to allow LaTeX builds | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Move the LaTeX preamble to a separate .tex file | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a typo in coqdomain.py | Clément Pit-Claudel | |
| 2018-09-19 | Move tests in bugs/ to the bugs/closed/. | Nick Lewycky | |
| 2018-09-19 | Fix Numeral Notations (4/4 - fixing synch) | Jason Gross | |
| This fixes #8401 Supersedes / closes #8407 Vernacular-command-registered numeral notations now live in the summary, and the interpretation function for them is hard-coded. Plugin-registered numeral notations are still unsynchronized, and only the UIDs of these functions gets synchronized. I am not 100% sure why this is fine, but the test-suite file working suggests that it is fine. I think it is because worker delegation correctly handles non-synchronized state which is declared at `Declare ML Module`-time. This final commit changes the synchronization of numeral notations (and deletes no-longer-used declarations in notation.mli that were introduced temporarily in the last commit). Since the interpretation can now be done in notation.ml, we no longer need to register unique ids for numeral notation (un)interp functions, and can instead synchronize the underlying constants with the document state. This is the change that actually fixes #8401. | |||
| 2018-09-19 | Fix Numeral Notations (3/4 - moving more stuff) | Jason Gross | |
| Move most of the rest of the stuff from numeral.ml to notation.ml. Now that we use exceptions to print error messages, all of the interpretation code for numeral notations can be moved to notation.ml. This is commit 1/4 in the fix for #8401. This is a pure cut/paste commit, modulo fixing name qualifications due to moved things, and exposing some stuff in notation.mli (to be removed in the next commit, where we finish the numeral notation reworking). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |