aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2019-05-15Merge PR #9905: [vm] x86_64 registersMaxime Dénès
Reviewed-by: maximedenes
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
We ungroup the rewrite scheme-defined constants, while only exporting a function to turn the last added constant into a private constant.
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it.
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ↵Maxime Dénès
specification Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-05-03Remove now useless commented codePierre Roux
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
There are three implementations of this primitive: * one in OCaml on 63 bits integer in kernel/uint63_amd64.ml * one in OCaml on Int64 in kernel/uint63_x86.ml * one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h Its specification is the axiom `diveucl_21_spec` in theories/Numbers/Cyclic/Int63/Int63.v * comment the implementations with loop invariants to enable an easy pen&paper proof of correctness (note to reviewers: the one in uint63_amd64.ml might be the easiest to read) * make sure the three implementations are equivalent * fix the specification in Int63.v (only the lowest part of the result is actually returned) * make a little optimisation in div21 enabled by the proof of correctness (cmp is computed at the end of the first loop rather than at the beginning, potentially saving one loop iteration while remaining correct) * update the proofs in Int63.v and Cyclic63.v to take into account the new specifiation of div21 * add a test
2019-05-02Add union in Map interfaceMaxime Dénès
2019-04-30Merge PR #9952: Remove `constr_of_global_in_context`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-30[vm] Backport from OCamlPierre Roux
Backport https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6 and https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e from OCaml VM
2019-04-30[vm] PPC64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785 from OCaml VM
2019-04-30[vm] ARM registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928 from OCaml VM
2019-04-30[vm] Arm 64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f from OCaml VM
2019-04-30[vm] x86_64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376 from OCaml VM
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-15[vm] Protect accu and coq_envPierre Roux
Protect accu and coq_env against GC calls in the VM when calling primitive integer functions on 32 bits architecture.
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
This is a step towards unifying the higher level ILs of the native and bytecode compilers. See https://github.com/coq/coq/projects/17
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
This function seems unused.
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp ↵Pierre-Marie Pédrot
skip_pattern Reviewed-by: ppedrot
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
This is convenient for the bootstrap of `coqdep`
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on ↵Gaëtan Gilbert
applications Reviewed-by: SkySkimmer
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
This fixes an incompleteness of subtyping on cumulative inductives, where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation depending on the variance of I's universe.
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
This takes advantage of the mutability of the fconstr relevance mark.
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:18:12 +0000