From 9c5a447688365006c8e594edfb1e973db8d53454 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 19 Mar 2018 14:13:01 +0100 Subject: Make parsing independent of the cumulativity flag. --- vernac/vernacentries.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'vernac/vernacentries.ml') 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 -- cgit v1.2.3