aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
2021-03-26Merge PR #11907: [zify] attempt to speed up look up of constrPierre-Marie Pédrot
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
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-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
2021-03-23Merge PR #13978: Do not match on record types with mutable fields in function...coqbot-app[bot]
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
2021-03-23Do not match on record types with mutable fields in function arguments.Guillaume Melquiond
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,...Andrej Dudenhefner
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
2021-03-22Move destRef outside ConstrMap.addBESSON Frederic
2021-03-22Merge PR #13225: Remove useless libobject for Implicit TypePierre-Marie Pédrot
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2021-03-22[cbn internal] env is a regular positional argumentGaëtan Gilbert
2021-03-22Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic.coqbot-app[bot]
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
2021-03-19[zify] Index by GlobRef instead constrBESSON Frederic
2021-03-19Remove useless libobject for Implicit TypeGaëtan Gilbert
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transit...Pierre-Marie Pédrot
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
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]
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
2021-03-16Merge PR #13920: Adding an Ltac2 API to manipulate inductive types.coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:02:41 +0000