aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * | | | | | | | | | | | | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | | | | Merge PR #6760: CHANGES for 8.7.2.Gravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | * Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
| * | | | | | | | | | | | | CHANGES for 8.7.2.Gravatar Théo Zimmermann2018-02-14
|/ / / / / / / / / / / / /
| | | | | | | | | * / / / Remove unused argument in Record.declare_structureGravatar Gaëtan Gilbert2018-02-14
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was for autoinstance.
| | | | | | | * | | | | Factorize the relocations in the on-disk VM representation.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * | | | | Use a more compact representation for bytecode relocations stored on disk.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * | | | | Do not use global variables for VM bytecode compilation in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead we thread a buffer.
| | | | | | | * | | | | Remove the unsafe bytes conversion function in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * | | | | Move the call to the computation of bytecode inside Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * | | | | Abstract further the type of VM bytecode compilation.Gravatar Pierre-Marie Pédrot2018-02-14
| |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reduces the possibility to wreak havoc while making the API nicer.
| | | | | | * | | | | detype_case predicate is not optionalGravatar Gaëtan Gilbert2018-02-14
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Gravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | |
| | | | | | * | | | | | [build] Fix VM dynamic linking prep in byte builds.Gravatar Emilio Jesus Gallego Arias2018-02-14
| | | | |_|/ / / / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We correctly set the path of `libcoqrun` in non-local builds. This bug was introduced by #6038. c.f. #6475 , #5992.
| | | | | | * | | | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (and alist-alist)
| | * | | | | | | | | Add CHANGES entry for #1047Gravatar Tej Chajed2018-02-13
| | |/ / / / / / / /
| | | | | * | | | | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | |
| | | | | * | | | | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | |
| | | | | * | | | | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | |
* | | | | | | | | | Merge PR #6693: [toplevel] Refactor command line argument handling.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | links (#6697)
* | | | | | | | | | | | | Merge PR #6738: CHANGES for universe varianceGravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | |_|_|/ / / | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | |
| | | * | | | | | | | | | | CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
| | | | | | | | | | | | | |
| | | | | | | | * | | | | | Add test case for #6677.Gravatar Maxime Dénès2018-02-12
| | | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | information.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6139: Make list functions returning sumbools transparentGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6718: Fix redirection to stderr in lint-repository error message.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6708: Mention -quiet flag for FailGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6706: ci-common: guess CI_BRANCH for local buildsGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6674: Delay computation of lifts in the reduction machine.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | | | Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism.
| | | | | | | | | * | | | | | | | | | | | | inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | Documentation for cumulative inductive variance.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | Print inductive cumulativity info in About.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
| | | | | | | | | | | | | | | | | | | * | | Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | * | | coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-08 16:54:54 +0000