aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | * | | | | [ocaml] [travis] Add preliminary 4.06 CI testing.Gravatar Emilio Jesus Gallego Arias2017-10-27
| |_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | We are still missing an updated LABLGTK.
| * | | | | | | | | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | | | | | Delay use of flag "Discriminate Introduction" from interp to execution time.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | |
| | | | | | | | * | Updating version history wrt 8.7.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | |
| | | | | | | | * | Updating version history wrt 8.6.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | |
| | | | | | | | * | Updating version history wrt 8.5.Gravatar Hugo Herbelin2017-10-26
| |_|_|_|_|_|_|/ / |/| | | | | | | |
| | | * | | | | | Rename \Tree to \NatTreeGravatar Johannes Kloos2017-10-25
| | | | | | | | |
| | | | | * | | | [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| | |_|_|/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
| | * | | | | | Moving from `is_true` to `= true`Gravatar Raphaël Monat2017-10-25
| | | | | | | |
| | | | | | | * Put linter at the top of the tests.Gravatar Théo Zimmermann2017-10-25
| | | | | | | |
| | | | | | | * Linter: check that files end with newlines.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use git check-attr to look at the same files as git diff --check.
| | | | | | | * Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | |
| | | | | | | * Add linter.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | |
* | | | | | | | Merge PR #6009: Master+misc typos dead code etcGravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6003: Point HoTT back at master, which now supports Coq masterGravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #5995: Revert "Add debug output to brew update."Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #5993: Switch testing branch back to CompCert upstream.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #5980: Add AppVeyor badge next to Travis badge.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #5971: [travis] Add flambda testing.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | |
| | | | | | | | | * | | | | Fix #5763: Strictly positive example is out of order.Gravatar jkloos2017-10-24
| |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example.
| | | | | | | * | | | | | Removing dead code which raised questions.Gravatar Hugo Herbelin2017-10-24
| | | | | | | | | | | | |
| | | | | | | * | | | | | Typo in comment in tactic_matching.ml.Gravatar Hugo Herbelin2017-10-24
| | | | | | | | | | | | |
| | | | | | | * | | | | | An occurrence of set_id which behaves as the identity.Gravatar Hugo Herbelin2017-10-24
| | | | | | | | | | | | |
| | | | | | | * | | | | | A missing newline after a comment.Gravatar Hugo Herbelin2017-10-24
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
| | | | | | | | * | | | Fix #4846Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | * | | | Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Made a description of unfold...in and moved the index entry there.
| | | | | | | | * | | | Documentation: Add various basic constructs to the index.Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was mentioned in #5631 as well. Now, forall, fun and casts have index entries.
| | | | | | | | * | | | Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As discussed in the bug report, this adds `(...) and `{...} to the index.
| | | | | | * | | | | Point HoTT back at master, which now supports Coq masterGravatar Jason Gross2017-10-23
| | | | | | | | | | |
| | | | | * | | | | | Move bug files to match their new GitHub ID (fixes #6001).Gravatar Théo Zimmermann2017-10-23
| |_|_|_|/ / / / / / |/| | | | | | | | |
| | | | | | | | * | Little code restructuration in CoqIDE tags.Gravatar Hugo Herbelin2017-10-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| | | | | | | | * | An attempt to fix issue #5771 (error color hidden by warning color).Gravatar Hugo Herbelin2017-10-22
| |_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | | | Revert "Add debug output to brew update."Gravatar Théo Zimmermann2017-10-20
| |_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | This reverts commit c7465d2ecb69e64613dd38b262f5e78ecad99de1.
| | | * | | | | Switch testing branch back to CompCert upstream.Gravatar Théo Zimmermann2017-10-20
| |_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | This follows the merge of AbsInt/CompCert#191.
* | | | | | | Merge PR #5989: Handle ∞ in coq-makefile timing test-suiteGravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | just Iris
* \ \ \ \ \ \ \ \ Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974).Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #5972: Fixing link to GitHub issue search, and wording.Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #1155: Use type nonrec in some functor arguments.Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1147: Remove GeoProof support.Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Gravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | clause of an inductive definitions
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1095: [stm] Remove state handling from FuturesGravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #960: Uniformize references to BugzillaGravatar Maxime Dénès2017-10-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |
| | | | | | | | * | | | | | | rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
| | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | Handle ∞ in coq-makefile timing test-suiteGravatar Jason Gross2017-10-19
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should (hopefully) fix #5675.
| * | | | | | | | | | | | | Moving bug numbers to BZ# format in the CHANGES file.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers.
| * | | | | | | | | | | | | Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
| * | | | | | | | | | | | | Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
|/ / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
| | | | | | | * / / / / / CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 01:46:18 +0000