diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-07-28 17:41:38 +0200 |
|---|---|---|
| committer | Amin Timany <amintimany@gmail.com> | 2017-07-31 18:05:54 +0200 |
| commit | e333c2fa6d97e79b389992412846adc71eb7abda (patch) | |
| tree | b3fc3e294820d72545f9647817e95eacf24422da /intf | |
| parent | 3b7e7f7738737475cb0f09130b0487c85906dd2b (diff) | |
Improve errors for cumulativity when monomorphic
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 6ef9532ad..2adf522b7 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -305,6 +305,14 @@ 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 + (** {6 The type of vernacular expressions} *) type vernac_expr = @@ -336,7 +344,7 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * (plident list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of |