From 8ff6ac9e0fa5ce5641ccc4b8e988ff9dbcc685ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jun 2018 15:35:02 -0700
Subject: [PATCH] refactor(kernel/environment): intro_rule ==> constructor

Lean is a programming language
---
 src/kernel/environment.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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<intro_rule>     m_intro_rules;
+    list<constructor>    m_constructors;
 };
 
 struct inductive_decls {