diff options
| author | Maxime Dénès | 2017-08-16 09:34:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:34:15 +0200 |
| commit | f0b4757d291ce3e07c8ccfcd4217d204fd2059ba (patch) | |
| tree | 3a2a3db40ab962e91366fca5223b6f25c390a276 /intf | |
| parent | 83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff) | |
| parent | 2f0e71c7e25eb193f252b6848dadff771dbc270d (diff) | |
Merge PR #864: Some cleanups after cumulativity for inductive types
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 6ef9532ad7..2adf522b74 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 |