aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
|
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
|
* Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
| | | | Was apparently forgotten in a67bd7f9.
* Again one more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2018-02-20
| | | | | | | | We enforce that variables of the notation hide the variables in the implicit-arguments map. Will be useful when there will be a special map of single binders when interpreting notations.
* Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Gravatar Maxime Dénès2018-02-19
|\ | | | | | | constraints.
* \ Merge PR #6761: Remove unused argument in Record.declare_structureGravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6230: Better Cemitcodes API + compact relocation representationGravatar Maxime Dénès2018-02-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6772: Cleanup inferCumulativityGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | camlp4
* \ \ \ \ \ \ \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6571: Fix ci-all targetGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | | | | * | | | | | | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| | | | | * | | | | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | No using a mutable counter to skip them, instead we keep them in the environment.
| | | | | * | | | | | | Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
| | | | | | | | | | * Adding a test for the construction that was broken in Coccinelle.Gravatar Pierre-Marie Pédrot2018-02-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was no test in the test-suite checking for double with-def constraints in module typing.
| | | | | | | | | | * Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
| | | | | | | * | | [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
| | | | | | | * | | [ide] Localize a IDE-specific flag.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |_|_|_|_|_|/ / / |/| | | | | | | |
* | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| | | | | | | | | |
| * | | | | | | | | also test vio2voGravatar Ralf Jung2018-02-15
| | | | | | | | | |
| * | | | | | | | | test "make quick2vo"Gravatar Ralf Jung2018-02-15
| | | | | | | | | |
| * | | | | | | | | new quick2vo target: like vio2vo, but smarterGravatar Ralf Jung2018-02-15
| | |_|_|/ / / / / | |/| | | | | | |
* | | | | | | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | 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
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | 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
|\ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 23:00:12 +0000