aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-26Be more thorough when testing PArray.set.Guillaume Melquiond
2021-03-26Improve dump of primitive OCaml operations.Guillaume Melquiond
2021-03-26Support OCaml primitives with an actual arity larger than 4.Guillaume Melquiond
PArray.set has arity 4, but due to the polymorphic universe, its actual arity is 5. As a consequence, Kshort_apply cannot be used to invoke it (or rather its accumulating version). Using Kapply does not quite work here, because Kpush_retaddr would have to be invoked before the arguments, that is, before we even know whether the arguments are accumulators. So, to use Kapply, one would need to push the return address, push duplicates of the already computed arguments, call the accumulator, and then pop the original arguments. This commit follows a simpler approach, but more restrictive, as it is still limited to arity 4, but this time independently from universes. To do so, the call is performed in two steps. First, a closure containing the universes is created. Second, the actual application to the original arguments is performed, for which Kshort_apply is sufficient. So, this is inefficient, because a closure is created just so that it can be immediately fully applied. But since this is the accumulator slow path, this does not matter.
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments.
2021-03-26Fix assertion that checks that APPLY can only be passed 4 arguments.Guillaume Melquiond
2021-03-26Split the return type away from the signature of primitive operations.Guillaume Melquiond
This avoids having to drop the last element of the signature in the common case.
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
Reviewed-by: silene
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26Similar fix for native compilation.Pierre-Marie Pédrot
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
Bytecode execution of persistent arrays can modify structured values meant to be marshalled in vo files. Some VM values are not marshallable, leading to this anomaly. There are further issues with the use of a hash table to store structured values, since they rely on structural equality and hashing functions. Persistent arrays are not safe in this context. Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
Reviewed-by: olaure01
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]
Reviewed-by: gares
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths ↵coqbot-app[bot]
to check for conversion Reviewed-by: gares Ack-by: SkySkimmer
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-26Expose less interface in coercionops.mliKazuhiko Sakaguchi
2021-03-25Merge PR #13988: Mention label name in signature mismatch error when ↵Pierre-Marie Pédrot
constant expected Reviewed-by: ppedrot
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
Fixes #14003: Ltac2 redefinition check is broken.
2021-03-25Merge PR #13989: fix documentation of Ltac2.Env.expandPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2021-03-24Merge PR #13993: iris_string_ident is no longer neededcoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-24Merge PR #13994: CI Quickchick: don't install quickchick executable to opamcoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-24CI Quickchick: don't install quickchick executable to opamGaëtan Gilbert
2021-03-24iris_string_ident is no longer neededRalf Jung
2021-03-24Merge PR #13981: Fix debug printersPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
Fix #13987
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-24Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ↵Pierre-Marie Pédrot
stack. Reviewed-by: ppedrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-23Merge PR #13978: Do not match on record types with mutable fields in ↵coqbot-app[bot]
function arguments. Reviewed-by: gares
2021-03-23fix documentation of Ltac2.Env.expandSamuel Gruetter
2021-03-23Fix debug printersGaëtan Gilbert
2021-03-23Merge PR #13974: [cbn internal] env is a regular positional argumentPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Do not match on record types with mutable fields in function arguments.Guillaume Melquiond
This tends to confuse the OCaml compiler, for good reasons. Indeed, if there are mutable fields, the generated code cannot wait for the function to be fully applied. It needs to recover the value of the mutable fields as early as possible, and thus to create a closure. Example: let foo {bar} x = ... is compiled as let foo y = match y with {bar} -> fun x -> ...
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-22Merge PR #13225: Remove useless libobject for Implicit TypePierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-22Factorize goal selector handlingGaëtan Gilbert
As a bonus ltac2 can produce bullet suggestions.
2021-03-22[cbn internal] env is a regular positional argumentGaëtan Gilbert
This is more consistent with other code.
2021-03-22Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
Fixes #13963
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
Reviewed-by: silene
2021-03-19Remove useless libobject for Implicit TypeGaëtan Gilbert
cache_function is called from add_leaf and after discharging sections, but default_object is section local.
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are ↵Pierre-Marie Pédrot
transitively closed Reviewed-by: ppedrot
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
2021-03-18Remove useless prefix argument in native compilation.Pierre-Marie Pédrot
2021-03-17Merge PR #13929: [ci] [gitlab] Remove ad-hoc mathcomp install macroscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:56:08 +0000