| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-13 | Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode. | Clément Pit-Claudel | |
| 2018-10-11 | Documenting -arg in _CoqProject. | Hugo Herbelin | |
| We follow Proof General documentation, section 11.2 "Using the Coq project file". | |||
| 2018-10-11 | Merge PR #186: [RFC] Coqlib cleanup | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #8384: Small fixes in attribute documentation. | Clément Pit-Claudel | |
| 2018-10-10 | [doc] [sphinx] Fix title levels. | Théo Zimmermann | |
| 2018-10-10 | Include all menu entries in the menu/short TOC so that users can view | Jim Fehrle | |
| menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents" | |||
| 2018-10-10 | Fix names for 2 entries in Flags, Options, Tables index. | Jim Fehrle | |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-09 | Refactoring of Micromega code using a Simplex linear solver | Frédéric Besson | |
| - Simplex based linear prover Unset Simplex to get Fourier elimination For lia and nia, do not enumerate but generate cutting planes. - Better non-linear support Factorisation of the non-linear pre-processing Careful handling of equation x=e, x is only eliminated if x is used linearly - More opaque interfaces (Linear solvers Simplex and Mfourier are independent) - Set Dump Arith "file" so that lia,nia calls generate Coq goals in filexxx.v. Used to collect benchmarks and regressions. - Rationalise the test-suite example.v only tests psatz Z example_nia.v only tests lia, nia In both files, the tests are in essence the same. In particular, if a test is solved by psatz but not by nia, we finish the goal by an explicit Abort. There are additional tests in example_nia.v which require specific integer reasoning out of scope of psatz. | |||
| 2018-10-05 | Rename CHANGES to CHANGES.md. | Guillaume Melquiond | |
| 2018-10-04 | Add missing indexes for Hint Cut and Hint Mode. | Théo Zimmermann | |
| 2018-10-03 | Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the ↵ | Théo Zimmermann | |
| compat updates to do as part of a release. | |||
| 2018-10-02 | Update the -compat flags | Jason Gross | |
| Mostly via `dev/tools/update-compat.py --cur-version=8.9` We just remove test-suite/success/FunindExtraction_compat86.v because, except for the `Extraction iszero.` line at the bottom, it is a duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`). We also manually update a number of test-suite files to pre-emptively remove compatibility notations (which used to be compat 8.6, but are now compat 8.7). | |||
| 2018-10-02 | [doc] Nits on utilities / toplevel building. | Emilio Jesus Gallego Arias | |
| 2018-10-01 | Docs: Missing backquote | Joachim Breitner | |
| 2018-10-01 | Merge PR #7634: Extend combined scheme to Schemes in Type | Matthieu Sozeau | |
| 2018-10-01 | Merge PR #8301: Documentation for proof diffs | Théo Zimmermann | |
| 2018-09-28 | Small fixes in attribute documentation. | Théo Zimmermann | |
| In particular, move the footnotes back to the foot of the chapter. | |||
| 2018-09-27 | Merge PR #8475: Centralize the reliance on abstract universe context internals | Gaëtan Gilbert | |
| 2018-09-26 | Merge PR #8504: Allow successive attributes #[foo] #[bar] | Vincent Laporte | |
| 2018-09-26 | Merge PR #8419: Remove romega in favor of lia | Théo Zimmermann | |
| 2018-09-26 | Allow successive attributes #[foo] #[bar] | Gaëtan Gilbert | |
| 2018-09-26 | Combined Scheme tests sort to use either "*" or "/\" | Théo Winterhalter | |
| And update documentation. | |||
| 2018-09-25 | Fix Sphinx manual targets. | Théo Zimmermann | |
| New targets refman, refman-html and refman-pdf. sphinx keeps its previous meaning (compatibility alias for refman-html). install-doc-sphinx has been accidentally renamed. | |||
| 2018-09-25 | Fix title of Introduction chapter in HTML version. | Théo Zimmermann | |
| And location of footnote. | |||
| 2018-09-25 | [doc] Rename credits-wrapper to credits and credits to credits-contents | Clément Pit-Claudel | |
| This ensures that previous links to 'credits.html' still point to the right page. | |||
| 2018-09-25 | [doc] Change Sphinx project title back to "Coq" | Clément Pit-Claudel | |
| Use 'The Coq Reference Manual' only in LaTeX. | |||
| 2018-09-25 | [doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJax | Clément Pit-Claudel | |
| 2018-09-25 | Remove romega | Vincent Laporte | |
| 2018-09-23 | Update flag, option and table descriptions in coqdomain.py, update ↵ | Jim Fehrle | |
| README.rst to match. Bump env_version. | |||
| 2018-09-23 | Documentation for proof diffs | Jim Fehrle | |
| 2018-09-21 | Universe binders are Id, not Name. Never print Var. | Gaëtan Gilbert | |
| Comes with minor cleanups in exception catching and unnecessary mapi. | |||
| 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-20 | Define flags (binary-valued settings) and tables (settings that are sets) | Jim Fehrle | |
| as separate NotationObject types, include in index. | |||
| 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? | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |