PPierre-Marie PédrotAbstract away the Summary reference type.
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Keep track of variable status (secvar or not) in named contexts Close #6773 | 3 个月前 | |
Add a deprecated option to restore the previous abstract behaviour. | 5 个月前 | |
Collapse sort variables to Prop if they are >= Prop but not <= Type Fix #22152 The "above prop" data in ustate now contains whether we only need `Prop <= q` or if `q <= Type` may be needed. Currently enforcing a constraint `q <= Type` actually forces `q == Type`, so `q <= Type` come from 2 cases: - template poly - when interpreting explicit `Type` in a potentially-template inductive (otherwise something like `Inductive I (P:Type -> ...) := C (_: P True)` produces `P:Prop -> ...`) | 2 个月前 | |
Remove duplicate warnings for missing all scheme | 2 个月前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 2 个月前 | |
Stop accepting non-globref hints from Hints. We now perform this check at the level of the tactics that call the underlying Hints API and simply ignore the hints when they are not globals. For backwards compatibility syntax-wise, we still allow expressions that evaluate to globrefs up to implicits. | 5 个月前 | |
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. | 22 天前 | |
Improve backwards compatibility by making `forward` optional | 2 个月前 | |
Distinguish unapplied functions from other terms in the dnet | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
cbn delayed subst | 2 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
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. | 22 天前 | |
parametrize typeclass functions with the db | 10 个月前 | |
Remove some spurious calls to pf_apply. | 9 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
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. | 22 天前 | |
Generalize DeclareScheme to use GlobRef instead of inductive prevent registering scheme for section variables without the local attribute | 5 个月前 | |
Remove unused API from Dn. | 5 年前 | |
Remove unused API from Dn. | 5 年前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 2 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
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. | 22 天前 | |
Add SProp case analysis scheme kinds (scase_dep, scase_nodep) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> | 5 个月前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Compute cross-scheme universe constraints explicitly Address review: instead of re-typechecking the hand-built schemes with Typing.type_of to recover the universe constraints missing from the hand-computed context sets, compute them explicitly. Since the schemes of an inductive type no longer share the universes standing for its template universes, the builders that apply a previously declared scheme (sym_involutive and l2r_rew, via const_of_scheme) must enforce the sorts of the parameters of the scheme being built to fit in the sorts of the corresponding binders of the applied constant, e.g. eq_rew_r_dep.u0 <= eq_sym.u0. These constraints were previously invisible because all schemes shared the default template levels (eq.u0 <= eq.u0). The other builders' context sets are self-contained: in particular, applications of template inductives (the inductive itself, and eq) need no constraints since the kernel instantiates them at application time; bugs/bug_22220.v now also tests this with a Type-sorted equality. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw | 2 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Merge PR #22079: Avoid printing missing-scheme warning when rewrite fails Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 3 个月前 | |
remove use of `option orientation` when only orientation is needed | 6 个月前 | |
Take a qualid in Evarnames.resolve. | 8 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Keep track of variable status (secvar or not) in named contexts Close #6773 | 3 个月前 | |
refactor fixpoint tactics | 1 年前 | |
Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
Added APIs for coqlsp | 5 个月前 | |
Added APIs for coqlsp | 5 个月前 | |
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. | 22 天前 | |
Remove the name field from projections. One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore. | 2 个月前 | |
Stop using global lazy in tactics/ | 3 个月前 | |
Deprecate the Coq-based APIs in Rocqlib. | 1 年前 | |
Collapse sort variables to Prop if they are >= Prop but not <= Type Fix #22152 The "above prop" data in ustate now contains whether we only need `Prop <= q` or if `q <= Type` may be needed. Currently enforcing a constraint `q <= Type` actually forces `q == Type`, so `q <= Type` come from 2 cases: - template poly - when interpreting explicit `Type` in a potentially-template inductive (otherwise something like `Inductive I (P:Type -> ...) := C (_: P True)` produces `P:Prop -> ...`) | 2 个月前 | |
generalize DeclareScheme from Constant.t to GlobRef.t | 9 个月前 | |
Fix generation of eliminators for not recursive inductive type but with non-unfiorm parameters | 2 个月前 | |
move indrec from pretpying/ to tactics/ | 8 个月前 | |
Rename is_section_variable' -> is_section_variable_env | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 3 个月前 | |
Remove the not extremely well-named Inv.inv function. It was only used once in funind and the function is easily reachable through the Inv.inv_clause wrapper. | 6 个月前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
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. | 22 天前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
Make the Genredexpr.red_expr_gen type open-ended. This makes it possible for plugins to extend the user-facing reductions with arbitrary code. Fixes #20979: Reductions in plugin. | 9 个月前 | |
Abstract the result type of rewrite strategies and modulify it. We never match on this type, it is only used to construct values fed to the rewriting engine. Furthermore, the internal implementation was very fragile because it duplicated the name of the constructors, requiring an explicitation of the type of the objects being manipulated. | 2 个月前 | |
Abstract the result type of rewrite strategies and modulify it. We never match on this type, it is only used to construct values fed to the rewriting engine. Furthermore, the internal implementation was very fragile because it duplicated the name of the constructors, requiring an explicitation of the type of the objects being manipulated. | 2 个月前 | |
Remove APIs that have been deprecated before 9.0. There are still a few that are actually used in the code. I left them around, for the lack of a better alternative. | 9 个月前 | |
Stdarg.wit_identref is vernac_genarg_type It doesn't have a registered intern so the glob and top types were incorrect and should be empty. | 7 个月前 | |
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> | 1 个月前 | |
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> | 1 个月前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 3 个月前 | |
Remove APIs that have been deprecated before 9.0. There are still a few that are actually used in the code. I left them around, for the lack of a better alternative. | 9 个月前 | |
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> | 1 个月前 | |
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> | 1 个月前 |