aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-20Merge PR #7868: [coqtop] Give priority to stdlib load path over current ↵Emilio Jesus Gallego Arias
directory
2018-06-19[coqtop] Give priority to stdlib load path over current directoryMaxime Dénès
When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail.
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-19Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Pierre-Marie Pédrot
2018-06-19Merge PR #7801: [vernac] Add option to force building really mutual ↵Enrico Tassi
induction schemes
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-19Merge PR #7714: Remove primitive-projection related data from the kernelMaxime Dénès
2018-06-19Merge PR #7856: Fix #7829: Spurious documentation failures.Maxime Dénès
2018-06-18Overlay for reference removalMaxime Dénès
2018-06-18Merge PR #7855: Update section on adding your project to CI and link to ↵Emilio Jesus Gallego Arias
example PR.
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
2018-06-18Remove Canary.whitequark
This eliminates 3 uses of Obj from TCB.
2018-06-18Fix #7829: Spurious documentation failures.Théo Zimmermann
We split a Require Import in two to avoid reaching the timeout.
2018-06-18Merge PR #7840: Remove Hashcons.HobjPierre-Marie Pédrot
2018-06-18Update section on adding your project to CI and link to example PR.Théo Zimmermann
2018-06-18Remove reference name type.Maxime Dénès
reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
2018-06-17Remove Hashcons.Hobj.whitequark
This eliminates 12 uses of Obj from TCB.
2018-06-17Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵Pierre-Marie Pédrot
to "match").
2018-06-17Merge PR #7848: Fix a typo in documentationThéo Zimmermann
2018-06-17Merge PR #7822: cArray: proper invalid_arg exceptionsPierre-Marie Pédrot
2018-06-17Merge PR #7844: Remove Elpi from Travis.Emilio Jesus Gallego Arias
2018-06-17Merge PR #7828: [Spawn] no control sock on unixEmilio Jesus Gallego Arias
2018-06-17Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingPierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel.
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time.
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless.
2018-06-17Merge PR #7749: [doc] Disable smartquotes conversionMaxime Dénès
2018-06-17Merge PR #7752: [merge script] Check if the CI that was run is outdated.Maxime Dénès
2018-06-17Merge PR #7635: Define rec_declaration in terms of prec_declaration.Maxime Dénès
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-16Remove Elpi from Travis.Théo Zimmermann
Rather than trying to keep the version of dependencies in sync with GitLab CI.
2018-06-16Merge PR #7814: doc: Add "Print Canonical Projections" command to Command indexThéo Zimmermann
2018-06-16[sphinx] Finish clean-up of the Canonical Structure subsection.Théo Zimmermann
2018-06-16doc: Add "Print Canonical Projections" command to Command indexAnton Trunov
2018-06-15[spawn] don't create a control socket on Unix (Fix #7713)Enrico Tassi
2018-06-15Add test-suite case for performance, had to use TimeoutMatthieu Sozeau
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible.
2018-06-15Merge PR #7813: Workaround for #2800: handling non-value arguments in tactics.Pierre-Marie Pédrot
2018-06-15Do not allow spliting in res_pf, this is reserved for pretypingMatthieu Sozeau
2018-06-15cArray: proper invalid_arg exceptionsMatthieu Sozeau
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
2018-06-14Merge PR #7803: [TYPO FIX] elimitate -> eliminateHugo Herbelin
2018-06-14Merge PR #7793: [ci] update docker image to include elpi 1.0.4Emilio Jesus Gallego Arias
2018-06-14Merge PR #7809: Fix deprecation warning introduced by PR 664 mergePierre-Marie Pédrot
2018-06-14Fix deprecation warning introduced by PR 664 mergeMatthieu Sozeau
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵Pierre-Marie Pédrot
of submodules.
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Matthieu Sozeau
to anomaly)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:51:07 +0000