diff --git a/src/kernel/environment.h b/src/kernel/environment.h index aff7bb15d9..e17450b836 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -100,12 +100,12 @@ public: bool is_descendant(environment_id const & id) const; }; -typedef expr intro_rule; +typedef expr constructor; struct inductive_decl { name m_name; expr m_type; - list m_intro_rules; + list m_constructors; }; struct inductive_decls {