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 /API/API.mli | |
| parent | 83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff) | |
| parent | 2f0e71c7e25eb193f252b6848dadff771dbc270d (diff) | |
Merge PR #864: Some cleanups after cumulativity for inductive types
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index a0e77edd12..a99cd2a9ae 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3782,6 +3782,12 @@ sig | DefaultInline | InlineAt of int + type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located @@ -3806,7 +3812,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of |