aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2017-10-17Adding a test for bug BZ#5692.Pierre-Marie Pédrot
2017-10-17unification: fix BZ#5692, recognize prim projs as CS projectionsMatthieu Sozeau
2017-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-10-17Handling primitive projections in canonical structures.Pierre-Marie Pédrot
2017-10-17[vernac] [state] Cache freeze/unfreezeEmilio Jesus Gallego Arias
Users need to be careful wrt global state modification outside `Vernacentries` without registering the functions. In particular, our fail implementation also has to invalidate the cache.
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
We still don't thread the state there, but this is a start of the needed infrastructure.
2017-10-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away.
2017-10-17[stm] First step to move interpretation of Undo commands out of the classifier.Emilio Jesus Gallego Arias
The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself.
2017-10-16Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`Maxime Dénès
2017-10-16Use type nonrec in some functor arguments.Gaëtan Gilbert
2017-10-16Merge PR #1152: Fix BZ#5785 (make install -j broken)Maxime Dénès
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
The test suite cases are preserved until the feature is actually removed.
2017-10-13Fix some more missing mkdir lines to Makefile.ideJason Gross
2017-10-13Fix BZ#5785 (make install -j broken)Jason Gross
This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between 8.6 and 8.7.
2017-10-13Merge PR #1103: Take Suggest Proof Using outside the kernel.Maxime Dénès
2017-10-12Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ↵Maxime Dénès
STM (BZ#5556)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-25 17:52:09 +0000