aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15new quick2vo target: like vio2vo, but smarterRalf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it.
2018-02-15Merge PR #6760: CHANGES for 8.7.2.Maxime Dénès
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
2018-02-14CHANGES for 8.7.2.Théo Zimmermann
2018-02-14Remove unused argument in Record.declare_structureGaëtan Gilbert
This was for autoinstance.
2018-02-14Factorize the relocations in the on-disk VM representation.Pierre-Marie Pédrot
Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to.
2018-02-14Use a more compact representation for bytecode relocations stored on disk.Pierre-Marie Pédrot
The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice.
2018-02-14Do not use global variables for VM bytecode compilation in Cemitcodes.Pierre-Marie Pédrot
Instead we thread a buffer.
2018-02-14Remove the unsafe bytes conversion function in Cemitcodes.Pierre-Marie Pédrot
This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way.
2018-02-14Move the call to the computation of bytecode inside Cemitcodes.Pierre-Marie Pédrot
This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode.
2018-02-14Abstract further the type of VM bytecode compilation.Pierre-Marie Pédrot
This reduces the possibility to wreak havoc while making the API nicer.
2018-02-14detype_case predicate is not optionalGaëtan Gilbert
2018-02-14Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Maxime Dénès
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-14adapt to Coq#6676Enrico Tassi
2018-02-14[coq] Adapt to coq/coq#6745Emilio Jesus Gallego Arias
Nothing remarkable.
2018-02-14[build] Fix VM dynamic linking prep in byte builds.Emilio Jesus Gallego Arias
We correctly set the path of `libcoqrun` in non-local builds. This bug was introduced by #6038. c.f. #6475 , #5992.
2018-02-13Fix issue with spurious timing test failuresJason Gross
When none of the numbers get over 100, the width of the table was different. See https://github.com/coq/coq/pull/6736#issuecomment-365386802
2018-02-13coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGaëtan Gilbert
(and alist-alist)
2018-02-13Add CHANGES entry for #1047Tej Chajed
2018-02-13coqdev.el: fix "compilate"-command typoGaëtan Gilbert
2018-02-13coqdev.el: shell-quote-argument the directory for make -CGaëtan Gilbert
2018-02-13coqdev.el: stop using when-let for emacs<25 compatibility.Gaëtan Gilbert
2018-02-13Fixing an anomaly in the presence of "let-in" in the type of a record.Hugo Herbelin
Was raised by Jason on Gitter.
2018-02-13Merge PR #6693: [toplevel] Refactor command line argument handling.Maxime Dénès
2018-02-13Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Maxime Dénès
2018-02-13Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Maxime Dénès
2018-02-13Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵Maxime Dénès
links (#6697)
2018-02-13Merge PR #6738: CHANGES for universe varianceMaxime Dénès
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
2018-02-12Add notation {x & P} for sigTTej Chajed
Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified.
2018-02-12Merge PR #6565: [Backport script] Check .mli files are not changed.Maxime Dénès
2018-02-12Tentative fix for #6520: camlcity.org unresponsive makes AppVeyor fail.Théo Zimmermann
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12CHANGES for universe varianceGaëtan Gilbert
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance ↵Maxime Dénès
information.
2018-02-12Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Maxime Dénès
2018-02-12Merge PR #6418: More detailed error messages for Canonical Structure, #6398Maxime Dénès
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-02-12Merge PR #6718: Fix redirection to stderr in lint-repository error message.Maxime Dénès
2018-02-12Merge PR #6708: Mention -quiet flag for FailMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 08:34:36 +0000