| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Merge PR #22074: Remove more global lazys Reviewed-by: ppedrot Reviewed-by: PierreCorbineau Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 2 个月前 | |
Report which terms are not convertible (#20944) `change False` and friends answered with a bare "Not convertible.", even though both terms are available at the point the error is raised. `NotConvertible` now carries optional data, following the pattern already used for similar errors in `vernac/himsg.ml`. The four call sites pass the terms they already have, and the message prints them when present: Error: Not convertible: "True" with "False". The wording follows the suggestion in the issue. When no terms are supplied the previous message is printed unchanged. Compatibility: the constructor gained an argument, so handlers matching on `TacticErrors.NotConvertible` (or the deprecated re-export `Tactics.NotConvertible`) need `NotConvertible _`. The one such handler in the tree, in `plugins/cc/cctac.ml`, is updated here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> | 30 天前 | |
Merge PR #21987: Keep track of which variables are section variables and use this info to fix bugs Reviewed-by: gares Ack-by: yannl35133 Co-authored-by: gares <gares@users.noreply.github.com> | 3 个月前 | |
Merge PR #22349: Fix singleton extraction after implicit erasure Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 7 天前 | |
Merge PR #22074: Remove more global lazys Reviewed-by: ppedrot Reviewed-by: PierreCorbineau Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 2 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Merge PR #22372: Abstract away the Summary reference type. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 19 天前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Merge PR #22074: Remove more global lazys Reviewed-by: ppedrot Reviewed-by: PierreCorbineau Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 2 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Merge PR #21955: Remove compat coq-core libraries (not executables) Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 3 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Make the ssrmatching occurrence type pure. Instead of storing references in a record, we wrap the record in a reference. Since we actually never expose those references, this reduces the number of behaviours of the inhabitants of the types. | 2 个月前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 20 天前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 |
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
| 2 个月前 | ||
| 30 天前 | ||
| 3 个月前 | ||
| 7 天前 | ||
| 2 个月前 | ||
| 20 天前 | ||
| 20 天前 | ||
| 19 天前 | ||
| 3 个月前 | ||
| 20 天前 | ||
| 2 个月前 | ||
| 20 天前 | ||
| 3 个月前 | ||
| 20 天前 | ||
| 2 个月前 | ||
| 20 天前 | ||
| 3 个月前 |