aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
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
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
Reviewed-by: gares
2021-03-16Merge PR #13920: Adding an Ltac2 API to manipulate inductive types.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-03-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-03-16add results on to_listOlivier Laurent
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:15:56 +0000