aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-10-26Delay use of flag "Discriminate Introduction" from interp to execution time.Hugo Herbelin
2017-10-26Updating version history wrt 8.7.Hugo Herbelin
2017-10-26Updating version history wrt 8.6.Hugo Herbelin
2017-10-26Updating version history wrt 8.5.Hugo Herbelin
2017-10-25Rename \Tree to \NatTreeJohannes Kloos
2017-10-25Use GHC.Base.Any for compatibility with GHC 8.2Tej Chajed
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-10-25Moving from `is_true` to `= true`Raphaël Monat
2017-10-25Put linter at the top of the tests.Théo Zimmermann
2017-10-25Linter: check that files end with newlines.Gaëtan Gilbert
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-25Add linter.Gaëtan Gilbert
2017-10-25Merge PR #6009: Master+misc typos dead code etcMaxime Dénès
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-25Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).Maxime Dénès
2017-10-25Merge PR #5995: Revert "Add debug output to brew update."Maxime Dénès
2017-10-25Merge PR #5993: Switch testing branch back to CompCert upstream.Maxime Dénès
2017-10-25Merge PR #5980: Add AppVeyor badge next to Travis badge.Maxime Dénès
2017-10-25Merge PR #5971: [travis] Add flambda testing.Maxime Dénès
2017-10-24Fix #5763: Strictly positive example is out of order.jkloos
2017-10-24Removing dead code which raised questions.Hugo Herbelin
2017-10-24Typo in comment in tactic_matching.ml.Hugo Herbelin
2017-10-24An occurrence of set_id which behaves as the identity.Hugo Herbelin
2017-10-24A missing newline after a comment.Hugo Herbelin
2017-10-24Fix #4846Johannes Kloos
2017-10-24Fix #5413: [unfold ... in] not documentedJohannes Kloos
2017-10-24Documentation: Add various basic constructs to the index.Johannes Kloos
2017-10-24Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Johannes Kloos
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-23Move bug files to match their new GitHub ID (fixes #6001).Théo Zimmermann
2017-10-22Little code restructuration in CoqIDE tags.Hugo Herbelin
2017-10-22An attempt to fix issue #5771 (error color hidden by warning color).Hugo Herbelin
2017-10-20Revert "Add debug output to brew update."Théo Zimmermann
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
2017-10-20Merge PR #5989: Handle ∞ in coq-makefile timing test-suiteMaxime Dénès
2017-10-20Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just...Maxime Dénès
2017-10-20Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974).Maxime Dénès
2017-10-20Merge PR #5972: Fixing link to GitHub issue search, and wording.Maxime Dénès
2017-10-20Merge PR #1155: Use type nonrec in some functor arguments.Maxime Dénès
2017-10-20Merge PR #1147: Remove GeoProof support.Maxime Dénès
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-20Merge PR #1095: [stm] Remove state handling from FuturesMaxime Dénès
2017-10-20Merge PR #960: Uniformize references to BugzillaMaxime Dénès
2017-10-19rename ci-iris-coq -> ci-iris-lambda-rustRalf Jung
2017-10-19Handle ∞ in coq-makefile timing test-suiteJason Gross
2017-10-19Moving bug numbers to BZ# format in the CHANGES file.Théo Zimmermann
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-08 17:20:26 +0000