From e333c2fa6d97e79b389992412846adc71eb7abda Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 28 Jul 2017 17:41:38 +0200 Subject: Improve errors for cumulativity when monomorphic We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. --- plugins/funind/glob_term_to_relation.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 379c83b24..e3010e3b5 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1471,7 +1471,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1486,7 +1486,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in -- cgit v1.2.3