From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 kernel/declareops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declareops.ml')

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;
-- 
cgit v1.2.3