aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-03Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ↵Maxime Dénès
color in coqide).
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Maxime Dénès
alphabet
2017-10-30Fixing #2881 ("change with" failing in an Ltac definition).Hugo Herbelin
We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards).
2017-10-27Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.Maxime Dénès
2017-10-27Merge PR #6015: [general] Remove Econstr dependency from `intf`Maxime Dénès
2017-10-27Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Maxime Dénès
2017-10-27Merge PR #5979: Fix #5763: Strictly positive example is out of order.Maxime Dénès
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-27Chaining two tactics in a proofRaphaël Monat
2017-10-27[ocaml] [travis] Add preliminary 4.06 CI testing.Emilio Jesus Gallego Arias
We are still missing an updated LABLGTK.
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
2017-10-26Delay use of flag "Discriminate Introduction" from interp to execution time.Hugo Herbelin
2017-10-25Rename \Tree to \NatTreeJohannes Kloos
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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 16:20:38 +0000