aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-16Adding an Ltac2 API to manipulate inductive types.Pierre-Marie Pédrot
Fixes #10095: Get list of constructors of Inductive.
2021-03-14Merge PR #13935: Fixed grammar productions for PDF documentationscoqbot-app[bot]
Reviewed-by: jfehrle
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
They should not be necessary today as they date from the shareable pre-artifact epoch, an incur in an slowdown.
2021-03-13Set the lsb of return addresses on the bytecode interpreter stack.Guillaume Melquiond
This makes it possible to skip the check when scanning the stack for the garbage collector.
2021-03-13Merge PR #13917: Add deriving lib to CI.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: SkySkimmer
2021-03-13Merge PR #13931: noglob/dumpglob should be in coqc specific usagecoqbot-app[bot]
Reviewed-by: gares Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:06:15 +0000