diff options
Diffstat (limited to 'kernel/declareops.ml')
-rw-r--r-- | kernel/declareops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 883896652..1d91b2d41 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -267,6 +267,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; + mind_cumulative = mib.mind_cumulative; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; |