coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/modops.ml

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 #22484: Substitute the values the resolver of an included application.
committed
Pierre-Marie Pédrot
Substitute the values the resolver of an included application.
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 #22451: Correctly implement δ-resolver lift for modules.
committed
Pierre-Marie Pédrot
Correctly implement δ-resolver lift for modules.
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
Pierre-Marie Pédrot
Remove non-monotonous operations from Mod_subst API.
committed
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 #21677: Improved handling of disabled VM
committed
Gaëtan Gilbert
VM error when encountering non compiled constant (from disabled VM)
committed
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
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
Stronger static invariant for Mod_subst.subst_dom_delta_resolver.
committed
coqbot-app[bot]
Merge PR #21703: Fix missing substitution in module aliasing.
committed
Pierre-Marie Pédrot
Fix missing substitution in module aliasing.
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 #21049: Check correctness of canonical constant and inductive names when typing.
committed
Pierre-Marie Pédrot
Store canonical constant and inductive names explicitly in environments.
committed
coqbot-app[bot]
Merge PR #21057: Fix substitution of functor delta-resolvers when performing strengthening
committed
Pierre-Marie Pédrot
Fix substitution of functor delta-resolvers when performing strengthening.
committed
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
coqbot-app[bot]
Merge PR #20999: Properly update resolvers of submodules when performing strengthening.
committed

August 2025

Pierre-Marie Pédrot
Properly update resolvers of submodules when performing strengthening.
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

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