| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | | | | Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition). |  Maxime Dénès | 2017-11-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ... | Maxime Dénès | 2017-11-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph... | Maxime Dénès | 2017-11-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | | | Update tactics.ml |  Farzon Lotfi | 2017-11-02 | |
| | |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | Ltac Debug: exporting env and sigma when needed so that term can be printed. |  Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Setting a system to register printers for Ltac values. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Exporting ValTMap for use in Genintern. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Using a specific function to register vernac printers. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Exporting the level-parametric printer of constr and its variants. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Do not identify a pre_ident as a string Ltac value. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Removing a redundancy in naming types (Ppconstr.precedence = tolerability). | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Naming the type of Dyn.Map for future reuse. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Exporting a few more printing functions. | Hugo Herbelin | 2017-11-02 | |
| | | | | | | | | | * | | | | | | | Improving checks about the list separator in tactic notations. | Hugo Herbelin | 2017-11-02 | |
| | |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | [API] Some reordering following latest separation commits. |  Emilio Jesus Gallego Arias | 2017-11-01 | |
| | | | | | | | | | | | | | | * | [general] Move Tactypes to `interp` | Emilio Jesus Gallego Arias | 2017-11-01 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | Fix FIXME: use OCaml 4.02 generative functors when available. |  Gaëtan Gilbert | 2017-11-01 | |
| | | | | | | | | | | | * | | | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules |  Matej Košík | 2017-11-01 | |
| | |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | Fixing #2881 ("change with" failing in an Ltac definition). | Hugo Herbelin | 2017-10-30 | |
| | | | | |_|_|_|_|/ / / / | | | |/| | | | | | | | | ||||
| | | | | | | | | | | | * | [ci] Switch VST back to upstream. |  Théo Zimmermann | 2017-10-30 | |
| | | | | | | | |_|_|_|/ | | | | | | |/| | | | | ||||
| | | | | | | | | * | | | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | 2017-10-28 | |
| | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
| | | | | | | | * | | | [toplevel] Export the last document seen after `Drop`. | Emilio Jesus Gallego Arias | 2017-10-28 | |
| | | | | |_|_|/ / / | | | |/| | | | | | ||||
| | | | | | | * | | | [ci] Switch back to upstream version of Math-Classes and Corn. | Théo Zimmermann | 2017-10-27 | |
| | | | | |_|/ / / | | | |/| | | | | ||||
| | | | | | * | | | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | Théo Zimmermann | 2017-10-27 | |
| | | | | |/ / / | | | |/| | | | ||||
| * | | | | | | | Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing. | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR #6015: [general] Remove Econstr dependency from `intf` | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ | Merge PR #5979: Fix #5763: Strictly positive example is out of order. | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #677: Trunk+abstracting injection flags | Maxime Dénès | 2017-10-27 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | * | | | | | | | | | | Chaining two tactics in a proof |  Raphaël Monat | 2017-10-27 | |
| | | | | | | * | | | | | | [ocaml] [travis] Add preliminary 4.06 CI testing. | Emilio Jesus Gallego Arias | 2017-10-27 | |
| | |_|_|_|_|/ / / / / / |/| | | | | | | | | | | ||||
| | * | | | | | | | | | | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | 2017-10-26 | |
| | * | | | | | | | | | | Delay use of flag "Discriminate Introduction" from interp to execution time. | Hugo Herbelin | 2017-10-26 | |
| | | | | | | | | * | | | Updating version history wrt 8.7. | Hugo Herbelin | 2017-10-26 | |
| | | | | | | | | * | | | Updating version history wrt 8.6. | Hugo Herbelin | 2017-10-26 | |
| | | | | | | | | * | | | Updating version history wrt 8.5. | Hugo Herbelin | 2017-10-26 | |
| | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
| | | | * | | | | | | | Rename \Tree to \NatTree |  Johannes Kloos | 2017-10-25 | |
| | | | | | * | | | | | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | 2017-10-25 | |
| | | |_|_|/ / / / / | |/| | | | | | | | ||||
| | | * | | | | | | | Moving from `is_true` to `= true` | Raphaël Monat | 2017-10-25 | |
| | | | | | | | * | | Put linter at the top of the tests. | Théo Zimmermann | 2017-10-25 | |
| | | | | | | | * | | Linter: check that files end with newlines. | Gaëtan Gilbert | 2017-10-25 | |
| | | | | | | | * | | Put newlines at the end of files. | Gaëtan Gilbert | 2017-10-25 | |
| | | | | | | | * | | Add linter. | Gaëtan Gilbert | 2017-10-25 | |
| * | | | | | | | | | Merge PR #6009: Master+misc typos dead code etc | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6003: Point HoTT back at master, which now supports Coq master | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001). | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #5995: Revert "Add debug output to brew update." | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #5993: Switch testing branch back to CompCert upstream. | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |