diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:06:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:36:08 +0200 |
| commit | 583c6c6204052ca177bc39d90b4aa7a645a90edc (patch) | |
| tree | d4a3c5287081b87a1eff54dcc4b11fa2c3c1b4df /vernac/comInductive.mli | |
| parent | 0bc7e7405553dc63d9693e85c3ce1485b5e8fe23 (diff) | |
[api] Reduce declare_kinds even more.
We remove two flags that were seldom used in favor of named parameters.
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 32 |
1 files changed, 20 insertions, 12 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 2d4cd7cac2..97f930c0a1 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -13,7 +13,6 @@ open Entries open Libnames open Vernacexpr open Constrexpr -open Decl_kinds (** {6 Inductive and coinductive types} *) @@ -23,11 +22,16 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -val do_mutual_inductive : - template:bool option -> universe_decl_expr option -> - (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> uniform:uniform_inductive_flag -> - Declarations.recursivity_kind -> unit +val do_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> (one_inductive_expr * decl_notation list) list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> uniform:uniform_inductive_flag + -> Declarations.recursivity_kind + -> unit (************************************************************************) (** Internal API *) @@ -71,12 +75,16 @@ val extract_mutual_inductive_declaration_components : structured_inductive_expr * (*coercions:*) qualid list * decl_notation list (** Typing mutual inductive definitions *) - -val interp_mutual_inductive : - template:bool option -> universe_decl_expr option -> structured_inductive_expr -> - decl_notation list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list +val interp_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> structured_inductive_expr + -> decl_notation list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> Declarations.recursivity_kind + -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |