| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | * | | | | 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 | |
| | | | | | | | | | | * | Use GHC.Base.Any for compatibility with GHC 8.2 |  Tej Chajed | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #5980: Add AppVeyor badge next to Travis badge. | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #5971: [travis] Add flambda testing. | Maxime Dénès | 2017-10-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | Fix #5763: Strictly positive example is out of order. | jkloos | 2017-10-24 | |
| | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | Removing dead code which raised questions. | Hugo Herbelin | 2017-10-24 | |
| | | | | | | | * | | | | | | | Typo in comment in tactic_matching.ml. | Hugo Herbelin | 2017-10-24 | |
| | | | | | | | * | | | | | | | An occurrence of set_id which behaves as the identity. | Hugo Herbelin | 2017-10-24 | |
| | | | | | | | * | | | | | | | A missing newline after a comment. | Hugo Herbelin | 2017-10-24 | |
| | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | Fix #4846 | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | * | | | | | Fix #5413: [unfold ... in] not documented | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | * | | | | | Documentation: Add various basic constructs to the index. | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | * | | | | | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | 2017-10-24 | |
| | |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | ||||
| | | | | | | * | | | | | | Point HoTT back at master, which now supports Coq master |  Jason Gross | 2017-10-23 | |
| | | | | | * | | | | | | | Move bug files to match their new GitHub ID (fixes #6001). | Théo Zimmermann | 2017-10-23 | |
| | |_|_|_|/ / / / / / / |/| | | | | | | | | | | ||||
| | | | | | | | | * | | | Little code restructuration in CoqIDE tags. | Hugo Herbelin | 2017-10-22 | |
| | | | | | | | | * | | | An attempt to fix issue #5771 (error color hidden by warning color). | Hugo Herbelin | 2017-10-22 | |
| | |_|_|_|_|_|_|/ / / |/| | | | | | | | | | ||||
| | | | | * | | | | | | Revert "Add debug output to brew update." | Théo Zimmermann | 2017-10-20 | |
| | |_|_|/ / / / / / |/| | | | | | | | | ||||
| | | | * | | | | | | Switch testing branch back to CompCert upstream. | Théo Zimmermann | 2017-10-20 | |
| | |_|/ / / / / / |/| | | | | | | | ||||
| * | | | | | | | | Merge PR #5989: Handle ∞ in coq-makefile timing test-suite | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just... | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ | Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974). | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #5972: Fixing link to GitHub issue search, and wording. | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1155: Use type nonrec in some functor arguments. | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1147: Remove GeoProof support. | Maxime Dénès | 2017-10-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |