diff options
| author | Gaëtan Gilbert | 2018-08-22 17:43:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:21:00 +0200 |
| commit | 69339f8fcfe3e5f3fa1c58feba6b0740c7e86538 (patch) | |
| tree | f09548fade8a03d2fb12edc6f58964dd25627eb1 /vernac/comInductive.mli | |
| parent | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (diff) | |
Fix #7754: universe declarations on mutual inductives
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 8a2c9b8719..f23085a538 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -24,7 +24,8 @@ type uniform_inductive_flag = | NonUniformParameters val do_mutual_inductive : - template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> polymorphic -> private_flag -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit @@ -54,7 +55,6 @@ val should_auto_template : unit -> bool type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -69,6 +69,7 @@ val extract_mutual_inductive_declaration_components : (** Typing mutual inductive definitions *) val interp_mutual_inductive : - template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> structured_inductive_expr -> + decl_notation list -> cumulative_inductive_flag -> polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list |