diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-19 14:13:01 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-21 15:51:42 +0100 |
| commit | 9c5a447688365006c8e594edfb1e973db8d53454 (patch) | |
| tree | 780e5bd2163f4af68c5d1e2144e432637301b838 /vernac/vernacentries.ml | |
| parent | f21deb6c861b359f0d3bf8b170d277cfa0d80171 (diff) | |
Make parsing independent of the cumulativity flag.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3dbe8b0c0..479f9725e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl = if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = - if poly then - match cum with - | GlobalCumulativity | LocalCumulativity -> true - | GlobalNonCumulativity | LocalNonCumulativity -> false - else - match cum with - | GlobalCumulativity | GlobalNonCumulativity -> false - | LocalCumulativity -> - user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | LocalNonCumulativity -> - user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + match cum with + | Some true -> + if poly then true + else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | Some false -> + if poly then false + else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + | None -> poly && Flags.is_polymorphic_inductive_cumulativity () let vernac_record cum k poly finite struc binders sort nameopt cfs = let is_cumulative = should_treat_as_cumulative cum poly in |