diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 10:04:07 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 10:04:07 +0200 |
| commit | 4c3564ac7e2ea231a6dde84f2af6bfddbc0834c6 (patch) | |
| tree | ba0f9bbbc04048c48a2128dde5bb89b2517e52c8 /vernac/vernacentries.ml | |
| parent | f97498a6c104da9b7b31f84505db76194a566f9b (diff) | |
| parent | bca95952b541b209a3f8ca44d1ff119b976e54fb (diff) | |
Merge PR #7016: Make parsing independent of the cumulativity flag.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0e8ca2289..b44c7cccb 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 VernacCumulative -> + if poly then true + else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | Some VernacNonCumulative -> + 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 @@ -565,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite let vernac_fixpoint ~atts discharge l = |