From cead81fcead24922b47b808f18fce9cef5c6bb20 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Jan 2019 16:47:28 +0100
Subject: [PATCH] fix(frontends/lean/inductive_cmds): set `m_explicit_levels`,
 and call `collect_implicit_locals` only after that

---
 src/frontends/lean/inductive_cmds.cpp | 8 +++++++-
 src/frontends/lean/inductive_cmds.h   | 2 +-
 src/frontends/lean/vm_elaborator.cpp  | 6 ------
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index d3a7421407..b906cd2bdc 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -777,11 +777,17 @@ environment inductive_cmd(parser & p, cmd_meta const & meta) {
 
 void elaborate_inductive_decls(parser & p, cmd_meta const & meta, buffer<decl_attributes> mut_attrs, buffer<name> lp_names,
                                name_map<implicit_infer_kind> implicit_infer_map,
-                               buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
+                               buffer<expr> params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
     inductive_cmd_fn fn(p, meta);
     fn.m_mut_attrs = mut_attrs;
     fn.m_lp_names = lp_names;
+    fn.m_explicit_levels = lp_names.size() || fn.has_explicit_level(intro_rules);
     fn.m_implicit_infer_map = implicit_infer_map;
+    buffer<expr> all_inds_intro_rules;
+    all_inds_intro_rules.append(inds);
+    for (buffer<expr> const & irs : intro_rules)
+        all_inds_intro_rules.append(irs);
+    collect_implicit_locals(p, fn.m_lp_names, params, all_inds_intro_rules);
     inductive_cmd_fn::parse_result r;
     fn.elaborate_inductive_decls(params, inds, intro_rules, r.m_params, r.m_inds, r.m_intro_rules);
     fn.add_inductive_decls(r);
diff --git a/src/frontends/lean/inductive_cmds.h b/src/frontends/lean/inductive_cmds.h
index 59d623ded4..e76392a292 100644
--- a/src/frontends/lean/inductive_cmds.h
+++ b/src/frontends/lean/inductive_cmds.h
@@ -14,7 +14,7 @@ environment inductive_cmd(parser & p, cmd_meta const & meta);
 
 void elaborate_inductive_decls(parser & p, cmd_meta const & meta, buffer<decl_attributes> mut_attrs, buffer<name> lp_names,
                                name_map<implicit_infer_kind> implicit_infer_map,
-                               buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules);
+                               buffer<expr> params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules);
 
 void register_inductive_cmds(cmd_table & r);
 void initialize_inductive_cmds();
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index 9d8cfe31b5..24e1c36904 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -288,12 +288,6 @@ static void elab_inductives_cmd(parser & p, expr const & cmd) {
         }
     }
 
-    buffer<expr> all_inds_intro_rules;
-    all_inds_intro_rules.append(inds);
-    for (buffer<expr> const & irs : intro_rules)
-        all_inds_intro_rules.append(irs);
-
-    collect_implicit_locals(p, lp_names, params, all_inds_intro_rules);
     elaborate_inductive_decls(p, meta, mut_attrs, lp_names, implicit_infer_map, params, inds, intro_rules);
 }