aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
2021-03-30Merge PR #13958: [recordops] complete API rewrite; the module is now called [...Pierre-Marie Pédrot
2021-03-30CI: don't output-syncGaëtan Gilbert
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:...coqbot-app[bot]
2021-03-29Merge PR #14025: [coqdep] remove leftover Caml stuff from man pagecoqbot-app[bot]
2021-03-29Print type of offending expression in Ltac2 not-unit warning.Pierre-Marie Pédrot
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
2021-03-26Merge PR #11907: [zify] attempt to speed up look up of constrPierre-Marie Pédrot
2021-03-26[doc] cleanup pretyping/structures.mliEnrico Tassi
2021-03-26Add non-performance-based testJason Gross
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
2021-03-26[ci] overlay file for #13958Enrico Tassi
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-26Document as critical.Guillaume Melquiond
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
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
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
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
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
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to...coqbot-app[bot]
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
2021-03-26Expose less interface in coercionops.mliKazuhiko Sakaguchi
2021-03-25Merge PR #13988: Mention label name in signature mismatch error when constant...Pierre-Marie Pédrot
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
2021-03-25Merge PR #13989: fix documentation of Ltac2.Env.expandPierre-Marie Pédrot
2021-03-24Merge PR #13993: iris_string_ident is no longer neededcoqbot-app[bot]
2021-03-24Merge PR #13994: CI Quickchick: don't install quickchick executable to opamcoqbot-app[bot]
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
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
2021-03-24Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ...Pierre-Marie Pédrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:30 +0000