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. --- intf/vernacexpr.ml | 10 +++------- parsing/g_vernac.ml4 | 10 ---------- plugins/funind/glob_term_to_relation.ml | 4 ++-- printing/ppvernac.ml | 5 +++-- vernac/vernacentries.ml | 19 ++++++++----------- 5 files changed, 16 insertions(+), 32 deletions(-) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index df061bfb7..df746f765 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -297,13 +297,9 @@ type inline = type module_ast_inl = module_ast * inline type module_binder = bool option * lident list * module_ast_inl -(** Cumulativity can be set globally, locally or unset locally and it - can not enabled at all. *) -type cumulative_inductive_parsing_flag = - | GlobalCumulativity - | GlobalNonCumulativity - | LocalCumulativity - | LocalNonCumulativity +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type cumulative_inductive_parsing_flag = bool option (** {6 The type of vernacular expressions} *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 72c3cc14a..7e7a887d3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -165,16 +165,6 @@ GEXTEND Gram indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - let cum = - match cum with - Some true -> LocalCumulativity - | Some false -> LocalNonCumulativity - | None -> - if Flags.is_polymorphic_inductive_cumulativity () then - GlobalCumulativity - else - GlobalNonCumulativity - in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (NoDischarge, recs) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 49f7aae43..319b410df 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1512,7 +1512,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1527,7 +1527,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5c5b7206a..b7f5a8309 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -788,8 +788,9 @@ open Decl_kinds if p then let cm = match cum with - | GlobalCumulativity | LocalCumulativity -> "Cumulative" - | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + | Some true -> "Cumulative" + | Some false -> "NonCumulative" + | None -> "" in cm ^ " " ^ kind else kind 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