| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-25 | Merge PR #9036: Add bodies to sphinx objects. | Clément Pit-Claudel | |
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-11-19 | Minor update to micromega.rst | soraros | |
| 2018-11-19 | Typo: comment does not match code | Olivier Laurent | |
| 2018-11-19 | Merge PR #9001: [options] Remove deprecated option automatic introduction. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8451: Print Universes Subgraph | Pierre-Marie Pédrot | |
| 2018-11-18 | [options] Remove deprecated option automatic introduction. | Emilio Jesus Gallego Arias | |
| 2018-11-16 | Print Universes Subgraph | Gaëtan Gilbert | |
| This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set). | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-16 | Merge PR #8888: Proof runcountable rebase | Hugo Herbelin | |
| 2018-11-07 | [doc] also scan plugins/ to build the lirbary index | Enrico Tassi | |
| 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 | Fix header and doc index | Vincent Semeria | |
| 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 #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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |