aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
To this extent we factor out the relevant bits to a new file, ltac_pretype.
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
We use git check-attr to look at the same files as git diff --check.
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
I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example.
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
Bug description: The "now" tactic, which is being used in the standard library, is not documented in the Reference Manual This commit documents the easy tactic, and gives now as a variant.
2017-10-24Fix #5413: [unfold ... in] not documentedJohannes Kloos
Made a description of unfold...in and moved the index entry there.
2017-10-24Documentation: Add various basic constructs to the index.Johannes Kloos
This was mentioned in #5631 as well. Now, forall, fun and casts have index entries.
2017-10-24Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Johannes Kloos
As discussed in the bug report, this adds `(...) and `{...} to the index.
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
- Removing tag "found" (unused since bd18c0821 "Now CoqIDE has a nice find & replace mechanism"). - Removing setting the priority of the debugging tag edit_zone: it was set at exactly the level it would have been by default minus 1, which is the level of tooltip, which have no associated visible markers, so the setting was a priori w/o effect. - For clarity, reorganizing order of tags into ephemere ones and non ephemere ones.
2017-10-22An attempt to fix issue #5771 (error color hidden by warning color).Hugo Herbelin
We change the relative priority of errors and warnings, so that the error takes precedence. It is unsure that it is universally the best choice. If the location of the error is finer than the one of the warning, it is better. In the other way round, it might be less good, e.g. if understanding the warning helps to understand the error. Maybe the best policy would be to test the relative locations of the warning and error? Trying to consider the error as more important, at the current time.
2017-10-20Revert "Add debug output to brew update."Théo Zimmermann
This reverts commit c7465d2ecb69e64613dd38b262f5e78ecad99de1.
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
This follows the merge of AbsInt/CompCert#191.
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 ↵Maxime Dénès
just Iris
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" ↵Maxime Dénès
clause of an inductive definitions
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
This should (hopefully) fix #5675.
2017-10-19Moving bug numbers to BZ# format in the CHANGES file.Théo Zimmermann
Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers.
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-19Add AppVeyor badge next to Travis badge.Théo Zimmermann
2017-10-18Bugzilla autolink: avoid linking inside links (fix #5974).Gaëtan Gilbert
2017-10-18Merge PR #984: Handling primitive projections in canonical structures.Maxime Dénès
2017-10-18Fixing link to GitHub issue search, and wording.Théo Zimmermann
2017-10-18[travis] Add flambda testing.Emilio Jesus Gallego Arias
2017-10-18Merge PR #1149: Moving to GitHub issues.Maxime Dénès
2017-10-18Moving to GitHub issues.Théo Zimmermann
This commit adds an issue template asking for version and OS information and adapts the contributing guide to the change of bug tracker.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 23:10:03 +0000