diff options
| author | Amin Timany | 2017-07-28 17:41:38 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | e333c2fa6d97e79b389992412846adc71eb7abda (patch) | |
| tree | b3fc3e294820d72545f9647817e95eacf24422da /plugins | |
| parent | 3b7e7f7738737475cb0f09130b0487c85906dd2b (diff) | |
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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 379c83b245..e3010e3b53 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 |