From b4012fdd71687490132afabbfcbd6b8a9e334eda Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Nov 2020 08:44:50 -0800 Subject: [PATCH] chore: remove old comment that is not true anymore --- src/kernel/inductive.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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;