PPierre-Marie PédrotAbstract away the Summary reference type.
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
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 个月前 | |
Move check_hyps_inclusion out of the kernel In the kernel we check the section variables used in another way (eg Constant_typing.check_section_variables) | 3 个月前 | |
Allow record syntax for record with anonymous fields For `Record foo := mk { x : nat ; y : 0 < x }.`, `{| x := 10 |}` already got turned into `mk 10 _`, so there is no reason to error if `y` was instead anonymous. We still error for ~~~coq Record foo := mk { x : nat ; _ : 0 < x }. Check {| bar with x := 10 |}. ~~~ since there is no constant for the needed projection. Close #4611 | 20 天前 | |
Allow record syntax for record with anonymous fields For `Record foo := mk { x : nat ; y : 0 < x }.`, `{| x := 10 |}` already got turned into `mk 10 _`, so there is no reason to error if `y` was instead anonymous. We still error for ~~~coq Record foo := mk { x : nat ; _ : 0 < x }. Check {| bar with x := 10 |}. ~~~ since there is no constant for the needed projection. Close #4611 | 20 天前 | |
Remove unnecessary removed_evars membership checks | 6 个月前 | |
Take a qualid in Evarnames.resolve. | 8 个月前 | |
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 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 个月前 | |
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 天前 | |
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 个月前 | |
rewrite logic_monad split in terms of run and reflect | 1 个月前 | |
Simplify list_view / reified types in logic_monad | 1 个月前 | |
Remove the dead Namegen.head_name function. | 2 个月前 | |
Remove the dead Namegen.head_name function. | 2 个月前 | |
Nameops.root_of_id don't fail on invalid idents ie if an ident built with of_string_soft is passed to this function it shouldn't cause a failure. | 7 个月前 | |
Add API Nameops.Fresh.union Efficiency isn't great because I couldn't grok SegTree enough to write an efficient union for it. | 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 | 8 个月前 | |
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 | 8 个月前 | |
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 天前 | |
Move ltac profiling cutoff away from global flags make it a goption and don't be imperative to set it in coqargs | 1 年前 | |
tclCASE use result instead of adhoc type | 1 个月前 | |
tclCASE use result instead of adhoc type | 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 | 8 个月前 | |
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 | 8 个月前 | |
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 个月前 | |
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 个月前 | |
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 天前 | |
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 个月前 | |
More precise type for UnivFlex.constrain_variables. | 8 个月前 | |
More precise type for UnivFlex.constrain_variables. | 8 个月前 | |
changed |= to | when displaying universes constraints | 2 个月前 | |
Avoid conflict between global sorts defined in separate modules We add a int uid to QGlobal.t, generated by safe_typing when adding the sort. The id is then useless so we remove it. The APIs change from combined `Global.push_qualities : QGlobal.Set.t * ElimConstraints.t -> unit` to separate `Global.new_global_sort : unit -> QGlobal.t` and `Global.merge_elim_constraints : ElimConstraints.t -> unit`. Fix #21717 | 4 个月前 | |
More precise type for UnivMinim.normalize_context_set. | 8 个月前 | |
More precise type for UnivMinim.normalize_context_set. | 8 个月前 | |
QGlobal is not QVar | 5 个月前 | |
QGlobal is not QVar | 5 个月前 | |
QLeq has nothing to do with elimination | 4 个月前 | |
feat: Add elim constraint elaboration Whenever an elimination constraint is not satisfied, then it adds the constraint as a new local one for the definition. Currently behind a flag to avoid backward compatibility for the moment. fix: Reintroduce QElimTo to univProblem It was replaced by QLeq to deal only with cumulativity constraints. refactor: Remove unnecessary abstraction of code Maybe it's using a more general API than it should, considering PConstraints instead of simply UnivConstrants. fix: Handle new EliminationError exception in cases and inductiveops print: Improve printing of qGraph and elimination errors refactor: Printing suggestions from code review Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> refactor: Printing suggestion | 7 个月前 | |
Remove the QCumulConstraint type for good. | 7 个月前 | |
Remove the QCumulConstraint type for good. | 7 个月前 |