| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-22 | Enable canonical `fun _ => _` projections. | Jan-Oliver Kaiser | |
| 2021-03-31 | Merge PR #14033: Properly expand projection parameters in Btermdn. | coqbot-app[bot] | |
| Reviewed-by: mattam82 | |||
| 2021-03-31 | Merge PR #14022: Replace mentions of Num by Zarith. | coqbot-app[bot] | |
| Reviewed-by: pi8027 | |||
| 2021-03-30 | Merge PR #11791: [flags] [profile] Remove bitrotten CProfile calls. | Pierre-Marie Pédrot | |
| Ack-by: gares Reviewed-by: ppedrot | |||
| 2021-03-30 | Properly expand projection parameters in Btermdn. | Pierre-Marie Pédrot | |
| The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections. | |||
| 2021-03-30 | [flags] [profile] Remove bit-rotten CProfile code. | Emilio Jesus Gallego Arias | |
| As of today Coq has the `CProfile` infrastructure disabled by default, untested, and not easily accessible. It was decided that `CProfile` should remain not user-accessible, and only available thus by manual editing of Coq code to switch the flag and manually instrument functions. We thus remove all bitrotten dead code. | |||
| 2021-03-30 | Merge PR #14012: Fix Ltac2 `Array.init` exponential overhead | Pierre-Marie Pédrot | |
| Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2021-03-30 | Merge PR #14005: Support OCaml primitives with an actual arity larger than 4. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-03-30 | Merge PR #13958: [recordops] complete API rewrite; the module is now called ↵ | Pierre-Marie Pédrot | |
| [structures] Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: herbelin Reviewed-by: ppedrot | |||
| 2021-03-30 | Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers. | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2021-03-29 | Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary ↵ | coqbot-app[bot] | |
| dependencies: Le, Gt, Minus, Lt, Setoid Reviewed-by: anton-trunov | |||
| 2021-03-29 | Merge PR #14025: [coqdep] remove leftover Caml stuff from man page | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2021-03-29 | Added a changelog. | Pierre-Marie Pédrot | |
| 2021-03-28 | [coqdep] remove leftover Caml stuff from man page | Hendrik Tews | |
| Dependencies for Caml files was removed in PR #11589, but some parts of it survived in the man page. | |||
| 2021-03-28 | Replace mentions of Num by Zarith. | Guillaume Melquiond | |
| The documentation of extraction became outdated when the big.ml wrapper got modified by 094e4649c29e2426daca0476c140439de901dafe. | |||
| 2021-03-26 | Merge PR #11907: [zify] attempt to speed up look up of constr | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2021-03-26 | [doc] cleanup pretyping/structures.mli | Enrico Tassi | |
| 2021-03-26 | Add non-performance-based test | Jason Gross | |
| 2021-03-26 | Add an Ltac1 to Ltac2 FFI for identifiers. | Pierre-Marie Pédrot | |
| Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented. Fixes #13996: missing Ltac1.to_ident. | |||
| 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 | |
| PArray.set has arity 4, but due to the polymorphic universe, its actual arity is 5. As a consequence, Kshort_apply cannot be used to invoke it (or rather its accumulating version). Using Kapply does not quite work here, because Kpush_retaddr would have to be invoked before the arguments, that is, before we even know whether the arguments are accumulators. So, to use Kapply, one would need to push the return address, push duplicates of the already computed arguments, call the accumulator, and then pop the original arguments. This commit follows a simpler approach, but more restrictive, as it is still limited to arity 4, but this time independently from universes. To do so, the call is performed in two steps. First, a closure containing the universes is created. Second, the actual application to the original arguments is performed, for which Kshort_apply is sufficient. So, this is inefficient, because a closure is created just so that it can be immediately fully applied. But since this is the accumulator slow path, this does not matter. | |||
| 2021-03-26 | Make it more obvious when the calling convention of APPLY changes. | Guillaume Melquiond | |
| Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments. | |||
| 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 | |
| This avoids having to drop the last element of the signature in the common case. | |||
| 2021-03-26 | Merge PR #14007: Never store persistent arrays as VM structured values. | coqbot-app[bot] | |
| Reviewed-by: silene | |||
| 2021-03-26 | Fix Ltac2 `Array.init` exponential overhead | Jason Gross | |
| Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011 | |||
| 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 | |
| Bytecode execution of persistent arrays can modify structured values meant to be marshalled in vo files. Some VM values are not marshallable, leading to this anomaly. There are further issues with the use of a hash table to store structured values, since they rely on structural equality and hashing functions. Persistent arrays are not safe in this context. Fixes #14006: Coqc cannot save .vo files containing primitive arrays. | |||
| 2021-03-26 | remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid | Andrej Dudenhefner | |
| fix unexpectedly broken MSetGenTree.v add changelog entry | |||
| 2021-03-26 | Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmas | coqbot-app[bot] | |
| Reviewed-by: olaure01 | |||
| 2021-03-25 | Merge PR #14004: Fix the redeclaration check for Ltac2 entry points. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2021-03-25 | Merge 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-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 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 ↵ | Pierre-Marie Pédrot | |
| constant expected Reviewed-by: ppedrot | |||
| 2021-03-25 | Fix the redeclaration check for Ltac2 entry points. | Pierre-Marie Pédrot | |
| Fixes #14003: Ltac2 redefinition check is broken. | |||
| 2021-03-25 | Merge PR #13989: fix documentation of Ltac2.Env.expand | Pierre-Marie Pédrot | |
| Reviewed-by: JasonGross Reviewed-by: ppedrot | |||
| 2021-03-24 | Merge PR #13993: iris_string_ident is no longer needed | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2021-03-24 | Merge PR #13994: CI Quickchick: don't install quickchick executable to opam | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 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 | |
| Reviewed-by: ppedrot | |||
| 2021-03-24 | Mention label name in signature mismatch error when constant expected | Gaëtan Gilbert | |
| Fix #13987 | |||
| 2021-03-24 | Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2 | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-03-24 | Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ↵ | Pierre-Marie Pédrot | |
| stack. Reviewed-by: ppedrot | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |