| Age | Commit message (Expand) | Author |
|---|
| 2021-03-30 | Merge PR #14005: Support OCaml primitives with an actual arity larger than 4. | Pierre-Marie Pédrot |
| 2021-03-30 | Merge PR #13958: [recordops] complete API rewrite; the module is now called [... | Pierre-Marie Pédrot |
| 2021-03-30 | Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers. | Michael Soegtrop |
| 2021-03-29 | Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:... | coqbot-app[bot] |
| 2021-03-29 | Merge PR #14025: [coqdep] remove leftover Caml stuff from man page | coqbot-app[bot] |
| 2021-03-29 | Added a changelog. | Pierre-Marie Pédrot |
| 2021-03-28 | [coqdep] remove leftover Caml stuff from man page | Hendrik Tews |
| 2021-03-26 | Merge PR #11907: [zify] attempt to speed up look up of constr | Pierre-Marie Pédrot |
| 2021-03-26 | [doc] cleanup pretyping/structures.mli | Enrico Tassi |
| 2021-03-26 | Add an Ltac1 to Ltac2 FFI for identifiers. | Pierre-Marie Pédrot |
| 2021-03-26 | [ci] overlay file for #13958 | Enrico Tassi |
| 2021-03-26 | [recordops] complete API rewrite; the module is now called [structures] | Enrico Tassi |
| 2021-03-26 | Document as critical. | Guillaume Melquiond |
| 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 | 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] |
