coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/mod_declarations.ml

October 2026

coqbot-app[bot]
Merge PR #22556: Correctly substitute module implementation δ-resolvers.
committed
Pierre-Marie Pédrot
Correctly substitute module implementation δ-resolvers.
committed

September 2026

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
coqbot-app[bot]
Merge PR #22418: Do not let an inclusion add an equivalence for the includer itself.
committed

August 2026

Pierre-Marie Pédrot
Do not let an inclusion add an equivalence for the includer itself.
committed

March 2026

coqbot-app[bot]
Merge PR #21716: Restrict retroknowledge declaration to toplevel.
committed
Pierre-Marie Pédrot
Restrict retroknowledge declaration to toplevel.
committed
coqbot-app[bot]
Merge PR #21705: Simplify module substitution API
committed
Pierre-Marie Pédrot
Remove the shallow module substitution API.
committed
Pierre-Marie Pédrot
Remove Mod_declaration.subst_dom and its implementation.
committed

October 2025

coqbot-app[bot]
Merge PR #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
committed

September 2025

coqbot-app[bot]
Merge PR #21048: Keep delta resolvers of sealed module bodies.
committed
Pierre-Marie Pédrot
Keep delta resolvers of sealed module bodies.
committed

July 2025

coqbot-app[bot]
Merge PR #20836: Names: move set/map modules `KNset` -> `KerName.Set` etc
committed
Gaëtan Gilbert
Names: move set/map modules `KNset` -> `KerName.Set` etc
committed

March 2025

coqbot-app[bot]
Merge PR #20344: Hashconsing try to avoid recomputing hashes
committed
Gaëtan Gilbert
Hashconsing try to avoid recomputing hashes
committed

January 2025

coqbot-app[bot]
Merge PR #20170: Additional cleanups around the module implementation
committed
Pierre-Marie Pédrot
Extrude an independent substitution function from a let-rec block.
committed
Pierre-Marie Pédrot
Defunctionalize substitutions in Mod_declarations.
committed
Pierre-Marie Pédrot
Add an API to get the global delta resolver out of a module.
committed
coqbot-app[bot]
Merge PR #20124: Stronger invariants in delta resolvers.
committed
Pierre-Marie Pédrot
Stronger invariants in delta resolvers.
committed
coqbot-app[bot]
Merge PR #20061: Remove unused module-related API.
committed
Pierre-Marie Pédrot
Remove unused module-related API.
committed
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 #20058: Ensure at runtime that the modpath is synced with module bodies and types
committed
Pierre-Marie Pédrot
Ensure at runtime that the modpath is synced with module bodies and types.
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
Make the generic_module_body type private.
committed
Pierre-Marie Pédrot
Consolidate module-mapping functions in Mod_declarations.
committed
Pierre-Marie Pédrot
Consolidate the module hashconsing functions in Mod_declarations.
committed
Pierre-Marie Pédrot
Move the module-related definitions from Declarations to a new module.
committed