coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/modops.mli

September 2026

coqbot-app[bot]
Merge PR #22494: Enforce more conditions in subtyping of inductive types.
committed
Pierre-Marie Pédrot
Enforce more conditions in subtyping of inductive types.
committed
coqbot-app[bot]
Merge PR #22493: Enforce that inductives have the same recursivity in subtyping.
committed
Pierre-Marie Pédrot
Enforce that inductives have the same recursivity in subtyping.
committed
coqbot-app[bot]
Merge PR #22472: Invert the aliasing declaration for inclusions of non-path modules.
committed
Pierre-Marie Pédrot
Invert the aliasing declaration for inclusions of non-path modules.
committed
coqbot-app[bot]
Merge PR #22446: Statically separate the three kinds of δ-resolvers.
committed
Pierre-Marie Pédrot
Statically separate the three kinds of δ-resolvers.
committed
coqbot-app[bot]
Merge PR #22353: Do not trust the serialized VM bytecode in rocqchk
committed
Archana Burra
Do not trust the serialized VM bytecode in rocqchk
committed

August 2026

coqbot-app[bot]
Merge PR #22394: Fix subtyping of inductives with letins in constructor types
committed
Gaëtan Gilbert
Fix subtyping of inductives with letins
committed

March 2026

coqbot-app[bot]
Merge PR #21737: Renamings, cleanup and UState.from_uctx which respects invariants
committed
Yann Leray
Change univ binder printer and create UState.from_auctx
committed

January 2026

coqbot-app[bot]
Merge PR #21465: Improve error messages around module typing issues
committed
Jason Gross
Improve error message for `with Definition` mod constraints
committed

December 2025

coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Rename Constraint(s) to UnivConstraint(s) for a more consistent naming
committed

October 2025

coqbot-app[bot]
Merge PR #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
committed
coqbot-app[bot]
Merge PR #20506: An elimination constraint graph to manage elimination of sort variables
committed
Johann Rosain
Use elimination graph at elaboration
committed

September 2025

coqbot-app[bot]
Merge PR #21043: Reduce the amount of casts between module bodies and types
committed
Pierre-Marie Pédrot
Remove useless aliases to the module cast functions.
committed

February 2025

coqbot-app[bot]
Merge PR #20182: Rename and tweak Modops.add_module_type.
committed
Pierre-Marie Pédrot
Rename and tweak Modops.add_module_type.
committed

January 2025

coqbot-app[bot]
Merge PR #20060: Stop storing the module path in modules.
committed
Pierre-Marie Pédrot
Stop storing the module path in modules.
committed
coqbot-app[bot]
Merge PR #19995: Abstract away the representation of module-related types
committed
Pierre-Marie Pédrot
Abstract away the various types of modules.
committed
Pierre-Marie Pédrot
Consolidate module-mapping functions in Mod_declarations.
committed
Pierre-Marie Pédrot
Move the module-related definitions from Declarations to a new module.
committed

December 2024

coqbot-app[bot]
Merge PR #19943: GADT-based representation of module / module types.
committed
Pierre-Marie Pédrot
GADT-based representation of module / module types.
committed

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

February 2024

coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Apply review suggestions
committed
Yann Leray
Add symbols, patterns, rewrite rule fields
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

March 2023

coqbot-app[bot]
Merge PR #17280: Print qualification information for module signature mismatch errors
committed

February 2023

Gaëtan Gilbert
Print qualification information for module signature mismatch errors
committed
Gaëtan Gilbert
Remove unused structure_field_body from SignatureMismatch error
committed

January 2023

coqbot-app[bot]
Merge PR #17049: Do not store the real functor argument type in Struct.
committed
Pierre-Marie Pédrot
Do not store the real functor argument type in Struct.
committed
coqbot-app[bot]
Merge PR #17007: Enforce that algebraic module expressions do not need functor arguments.
committed

December 2022

Pierre-Marie Pédrot
Enforce that algebraic module expressions do not need functor arguments.
committed

March 2022

coqbot-app[bot]
Merge PR #15856: Remove the univ_of_sort function from the API.
committed
Pierre-Marie Pédrot
Move UniverseInconsistency from Univ to UGraph.
committed