diff options
| author | Pierre-Marie Pédrot | 2016-06-17 20:26:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 18:54:43 +0200 |
| commit | ecb032467557631ea60324c6afa55c91c133e40d (patch) | |
| tree | 831803ca1db0e73ec3cea91c52f5f2e288d12341 /toplevel/command.mli | |
| parent | 53ced0735f7e24735d78a02fc74588b8d9186eab (diff) | |
Reuse the typing_flags datatype for inductives.
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index a5132cc664..d353724294 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -91,7 +91,6 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : - bool -> (* if [false], then positivity is assumed *) structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list @@ -106,7 +105,6 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : - bool -> (* if [false], then positivity is assumed *) (one_inductive_expr * decl_notation list) list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit |