diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-22 13:21:41 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-22 13:21:41 +0100 |
| commit | bca95952b541b209a3f8ca44d1ff119b976e54fb (patch) | |
| tree | cc4f6d8a466a0862a8fa3b4c0db8beef4a4c43c8 /vernac/vernacentries.ml | |
| parent | 9c5a447688365006c8e594edfb1e973db8d53454 (diff) | |
bool option -> (VernacCumulative | VernacNonCumulative) option
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 479f9725e..1f6f9fa98 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -535,10 +535,10 @@ let vernac_assumption ~atts discharge kind l nl = let should_treat_as_cumulative cum poly = match cum with - | Some true -> + | Some VernacCumulative -> if poly then true else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | Some false -> + | 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 () @@ -562,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 @@ -599,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 = |