aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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)
2017-10-12Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Maxime Dénès
directory` on every execution
2017-10-11Remove GeoProof support.Maxime Dénès
Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
2017-10-11Merge PR #1054: Restoring test on ident validity while browsing directory ↵Maxime Dénès
structure.
2017-10-11Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Maxime Dénès
execution
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
We move delicate library/module instillation code to the STM so the API guarantees that the first state snapshot is correct. That was not the case in the past, which meant that the STM cache was unsound in batch mode, however we never used its contents due to not backtracking to the first state. This provides quite an improvement in the API, however more work is needed until the codepath is fully polished. This is a critical step towards handling the STM functionally.
2017-10-11Merge PR #1143: fix coq_makefile on cygwinMaxime Dénès
2017-10-10Stm.get_hint_ctx: remove unused Str.splitGaëtan Gilbert
With suggest proof using out of the kernel the format of context_used in .aux is just the list of ids wanted by get_hint_ctx. (split x s when x doesn't appear in s just returns the singleton list [s])
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Code factorization Vernacentries.interp on VernacProof.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:16:46 +0000