diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 0489c2f14a..cdc38ceb12 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -70,10 +70,7 @@ optional get_rec_rule_for(recursor_val const & rec_val, expr cons return optional(); } -/* Auxiliary class for adding a mutual inductive datatype declaration. - - \remak It does not support nested inductive datatypes. The helper - class elim_nested_inductive_fn should be used as a preprocessing step. */ +/* Auxiliary class for adding a mutual inductive datatype declaration. */ class add_inductive_fn { environment m_env; name_generator m_ngen;