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

---
 library/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index bf5313545c..e2b726f457 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -352,13 +352,14 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
+  mind_entry_cumulative = false;
   mind_entry_universes = Univ.UInfoInd.empty;
   mind_entry_private = None;
 })
 
 (* reinfer subtyping constraints for inductive after section is dischared. *)
 let infer_inductive_subtyping (pth, mind_ent) = 
-  if mind_ent.mind_entry_polymorphic then
+  if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then
     begin
       let env = Global.env () in
       let env' =
@@ -370,7 +371,6 @@ let infer_inductive_subtyping (pth, mind_ent) =
     end
   else (pth, mind_ent)
 
-
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
 let inInductive : inductive_obj -> obj =
-- 
cgit v1.2.3