| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-06 | Improve rendering of the credits. | Guillaume Melquiond | |
| This mostly fixes text that was italicized instead of teletyped. When possible, tactic names have been made to point to their documentation. Also, the date of the 8.9 release has been proactively changed to November. | |||
| 2018-11-01 | Merge PR #8845: Fix typos in the document about CIC | Théo Zimmermann | |
| 2018-10-30 | Credits for 8.9 | Matthieu Sozeau | |
| Adressed comments by Guillaume and Jason Updated according to Zimmi48's input. Better link to custom entries Fix typesetting | |||
| 2018-10-29 | Fix typos in the document about CIC | wkwkes | |
| 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 #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-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-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 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |