aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
This fixes also #5731, #6035, #5364.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:30:32 +0000