| Age | Commit message (Expand) | Author |
|---|
| 2021-03-26 | Be more thorough when testing PArray.set. | Guillaume Melquiond |
| 2021-03-26 | Improve dump of primitive OCaml operations. | Guillaume Melquiond |
| 2021-03-26 | Support OCaml primitives with an actual arity larger than 4. | Guillaume Melquiond |
| 2021-03-26 | Make it more obvious when the calling convention of APPLY changes. | Guillaume Melquiond |
| 2021-03-26 | Fix assertion that checks that APPLY can only be passed 4 arguments. | Guillaume Melquiond |
| 2021-03-26 | Split the return type away from the signature of primitive operations. | Guillaume Melquiond |
| 2021-03-26 | Merge PR #14007: Never store persistent arrays as VM structured values. | coqbot-app[bot] |
| 2021-03-26 | Fix Ltac2 `Array.init` exponential overhead | Jason Gross |
| 2021-03-26 | Adding a changelog. | Pierre-Marie Pédrot |
| 2021-03-26 | Similar fix for native compilation. | Pierre-Marie Pédrot |
| 2021-03-26 | Never store persistent arrays as VM structured values. | Pierre-Marie Pédrot |
| 2021-03-26 | remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid | Andrej Dudenhefner |
| 2021-03-26 | Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmas | coqbot-app[bot] |
| 2021-03-25 | Merge PR #14004: Fix the redeclaration check for Ltac2 entry points. | coqbot-app[bot] |
| 2021-03-25 | Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to... | coqbot-app[bot] |
| 2021-03-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] |
| 2021-03-26 | Expose less interface in coercionops.mli | Kazuhiko Sakaguchi |
| 2021-03-25 | Merge PR #13988: Mention label name in signature mismatch error when constant... | Pierre-Marie Pédrot |
| 2021-03-25 | Fix the redeclaration check for Ltac2 entry points. | Pierre-Marie Pédrot |
| 2021-03-25 | Merge PR #13989: fix documentation of Ltac2.Env.expand | Pierre-Marie Pédrot |
| 2021-03-24 | Merge PR #13993: iris_string_ident is no longer needed | coqbot-app[bot] |
| 2021-03-24 | Merge PR #13994: CI Quickchick: don't install quickchick executable to opam | coqbot-app[bot] |
| 2021-03-24 | CI Quickchick: don't install quickchick executable to opam | Gaëtan Gilbert |
| 2021-03-24 | iris_string_ident is no longer needed | Ralf Jung |
| 2021-03-24 | Merge PR #13981: Fix debug printers | Pierre-Marie Pédrot |
| 2021-03-24 | Mention label name in signature mismatch error when constant expected | Gaëtan Gilbert |
| 2021-03-24 | Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2 | Pierre-Marie Pédrot |
| 2021-03-24 | Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ... | Pierre-Marie Pédrot |
| 2021-03-24 | Merge PR #13973: Factorize goal selector handling | Pierre-Marie Pédrot |
| 2021-03-23 | Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat... | Michael Soegtrop |
| 2021-03-23 | Merge PR #13914: Allow the presence of type casts for return values in Ltac2. | Michael Soegtrop |
| 2021-03-23 | Merge PR #13978: Do not match on record types with mutable fields in function... | coqbot-app[bot] |
| 2021-03-23 | fix documentation of Ltac2.Env.expand | Samuel Gruetter |
| 2021-03-23 | Fix debug printers | Gaëtan Gilbert |
| 2021-03-23 | Merge PR #13974: [cbn internal] env is a regular positional argument | Pierre-Marie Pédrot |
| 2021-03-23 | Do not match on record types with mutable fields in function arguments. | Guillaume Melquiond |
| 2021-03-23 | add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,... | Andrej Dudenhefner |
| 2021-03-23 | Merge PR #13671: [stdlib] [Vectors] add results on to_list | coqbot-app[bot] |
| 2021-03-23 | Merge PR #13804: [stdlib] [List] Add results about count_occ | coqbot-app[bot] |
| 2021-03-22 | Move destRef outside ConstrMap.add | BESSON Frederic |
| 2021-03-22 | Merge PR #13225: Remove useless libobject for Implicit Type | Pierre-Marie Pédrot |
| 2021-03-22 | Factorize goal selector handling | Gaëtan Gilbert |
| 2021-03-22 | [cbn internal] env is a regular positional argument | Gaëtan Gilbert |
| 2021-03-22 | Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic. | coqbot-app[bot] |
| 2021-03-22 | Merge PR #13961: Implement ! goal selector for Ltac2. | coqbot-app[bot] |
| 2021-03-19 | implement is_const, is_var, ... etc and has_evar for Ltac2 | Samuel Gruetter |
| 2021-03-19 | Merge PR #13956: Remove useless prefix argument in native compilation. | coqbot-app[bot] |
| 2021-03-19 | [zify] Index by GlobRef instead constr | BESSON Frederic |
| 2021-03-19 | Remove useless libobject for Implicit Type | Gaëtan Gilbert |
| 2021-03-19 | Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transit... | Pierre-Marie Pédrot |
