GGaëtan GilbertIntroduce "Univ@{s;l}" notation for sort polymorphism
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
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. | 1 个月前 | |
Extend and cleanup the abbreviation API. | 11 个月前 | |
Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s` This also makes it stop relying on level tolerance. Fix #22324 | 1 个月前 | |
Introduce "Univ@{s;l}" notation for sort polymorphism Deprecated old interpretations of Type as Univ (with quickfix) Adapt test-suite to deprecation and update output tests ("breaking" output change) Fix make_anonymous_conclusion_flexible to support `Univ` Add changelog Update documentation of univ-poly Fixup Fix refman Fix typo Stop interpreting Type as Univ. Fix doc, useless if-then-else | 6 天前 | |
Introduce "Univ@{s;l}" notation for sort polymorphism Deprecated old interpretations of Type as Univ (with quickfix) Adapt test-suite to deprecation and update output tests ("breaking" output change) Fix make_anonymous_conclusion_flexible to support `Univ` Add changelog Update documentation of univ-poly Fixup Fix refman Fix typo Stop interpreting Type as Univ. Fix doc, useless if-then-else | 6 天前 | |
Implement `{| foo with fields |}` for terms Fix #14438 Co-authored-by: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com> | 2 个月前 | |
Pass printing flags functionally in constr printers | 10 个月前 | |
GenConstr can intern directly to constr | 1 个月前 | |
Merge PR #22207: Implement `{| foo with fields |}` for terms Reviewed-by: cpitclaudel Reviewed-by: ppedrot 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. | 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 年前 | |
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. | 1 个月前 | |
Use quotiented constant maps in Dumpglob. | 4 个月前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 4 个月前 | |
GenConstr can intern directly to constr | 1 个月前 | |
GenConstr can intern directly to constr | 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. | 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 年前 | |
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. | 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 年前 | |
Introduce PolyFlags to gather flags for polymorphic defs Adapt the whole code base to using this instead of the multiple poly/sort_poly/cumulative flags. poly_flags -> poly PolyFlags.of_poly -> of_level_poly sort_polymorphic -> implicit_sort_polymorphic Implement suggested fixes from PR level_polymorphic -> univ_polymorphic implicit_sort_polymorphic -> collapse_sorts_to_type univ_polymorphic -> univ_poly cleaner parsing of attributes (cumulative and collapse_sort_variables are just not settable without universe polymorphism). Fixed comments Apply suggestions from code review Spacing/indentation Co-authored-by: yannl35133 <40719961+yannl35133@users.noreply.github.com> Fix wrong poly kind used for inductive and record decls Remove options that are not supported yet Add Changelog entry PolyFlags.assumption_or_definition -> PolyFlags.construction_kind Support the polymorphism attributes in Hint Rewrite Change plugin_tutorial to use the forward-compatible poly_def attribute Add overlays Fix rewrite rule integration of polyflags as per Y. Leray's comments Add debug printer | 9 个月前 | |
Revert name change of univ_decl to sort_poly_decl | 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. | 1 个月前 | |
add location notation information | 2 个月前 | |
QGlobal is not QVar | 6 个月前 | |
Pass printing flags functionally in constr printers | 10 个月前 | |
Merge PR #21574: Stop using genarg for constr syntax extension Reviewed-by: proux01 Co-authored-by: proux01 <proux01@users.noreply.github.com> | 7 个月前 | |
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. | 1 个月前 | |
Stop relying on CanOrd in Notationextern. | 1 年前 | |
Fully separate ltac2 notation parsing from intern-time data | 6 个月前 | |
Fully separate ltac2 notation parsing from intern-time data | 6 个月前 | |
Use the VM for primitive token normalization. We have to set the parameter normalization flag to be sure everything works as before. | 3 个月前 | |
Pass printing flags functionally in constr printers | 10 个月前 | |
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. | 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 年前 | |
Extend and cleanup the abbreviation API. | 11 个月前 | |
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 年前 |