| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-24 | Merge PR #8813: Fix a few rendering issues in the manual | Théo Zimmermann | |
| 2018-10-24 | Merge PR #8776: Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends" | Théo Zimmermann | |
| 2018-10-24 | [Manual] Prevent an irrelevant warning to show up | Vincent Laporte | |
| 2018-10-24 | [Manual] Avoid using deprecated “Focus” | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix rendering of an example | Vincent Laporte | |
| 2018-10-24 | [Manual] Typo | Vincent Laporte | |
| 2018-10-24 | [Manual] Fix an example | Vincent Laporte | |
| The `Undo` command is not reliable. | |||
| 2018-10-24 | [Manual] Fix layout of a list | Vincent Laporte | |
| 2018-10-23 | Merge PR #8365: Strings: add ByteVector | Hugo Herbelin | |
| 2018-10-23 | Merge PR #8798: Order Greek letters consistently w/rest of document | Théo Zimmermann | |
| 2018-10-23 | Fix formatting. Use standard if..then grammar. | Sam Pablo Kuper | |
| 2018-10-23 | Order Greek letters consistently w/rest of document | Sam Pablo Kuper | |
| 2018-10-19 | Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends" | Sam Pablo Kuper | |
| 2018-10-17 | doc: mention ByteVector | Yishuai Li | |
| 2018-10-16 | Document the issue with positive coinductive types. | Pierre-Marie Pédrot | |
| 2018-10-15 | Correct some spelling errors | Benjamin Barenblat | |
| Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. | |||
| 2018-10-13 | Merge PR #8616: Include the full Table of Contents document in the on-screen ↵ | Clément Pit-Claudel | |
| TOC, ... | |||
| 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: | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |