diff options
| -rw-r--r-- | intf/vernacexpr.ml | 4 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
4 files changed, 10 insertions, 9 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index df746f765..c1c80b61d 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -299,7 +299,7 @@ type module_binder = bool option * lident list * module_ast_inl (** [Some b] if locally enabled/disabled according to [b], [None] if we should use the global flag. *) -type cumulative_inductive_parsing_flag = bool option +type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) @@ -334,7 +334,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7e7a887d3..b947253b7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -161,7 +161,7 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) (* Gallina inductive declarations *) - | cum = cumulativity_token; priv = private_token; f = finite_token; + | cum = OPT cumulativity_token; priv = private_token; f = finite_token; 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 @@ -247,7 +247,8 @@ GEXTEND Gram | IDENT "Class" -> (Class true,BiFinite) ] ] ; cumulativity_token: - [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + [ [ IDENT "Cumulative" -> VernacCumulative + | IDENT "NonCumulative" -> VernacNonCumulative ] ] ; private_token: [ [ IDENT "Private" -> true | -> false ] ] diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index b7f5a8309..8180e4503 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -788,8 +788,8 @@ open Decl_kinds if p then let cm = match cum with - | Some true -> "Cumulative" - | Some false -> "NonCumulative" + | Some VernacCumulative -> "Cumulative" + | Some VernacNonCumulative -> "NonCumulative" | None -> "" in cm ^ " " ^ kind 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 = |