From 8ea2bc08cb03b49f61db90c28115dfa9f4d09410 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 11 Apr 2017 13:33:07 +0200
Subject: [PATCH] feat(init/meta/interactive): add `generalizing` parameter to
 `induction`

---
 library/init/meta/interactive.lean     | 9 +++++++--
 library/init/meta/smt/interactive.lean | 5 +++--
 src/frontends/lean/token_table.cpp     | 2 +-
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 609268af31..b62328edd4 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -336,8 +336,13 @@ do e_type ← infer_type e >>= whnf,
    (const I ls) ← return $ get_app_fn e_type,
    return I
 
-meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
-do e ← i_to_expr p, tactic.induction e ids rec_name, return ()
+meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
+  (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
+do e ← i_to_expr p,
+   locals ← get_locals $ revert.get_or_else [],
+   n ← revert_lst locals,
+   tactic.induction e ids rec_name,
+   all_goals (intron n)
 
 meta def cases (p : parse texpr) (ids : parse with_ident_list) : tactic unit :=
 do e ← i_to_expr p,
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index bf81812424..e4f9c30880 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -219,8 +219,9 @@ smt_tactic.repeat t
 meta def all_goals (t : itactic) : smt_tactic unit :=
 smt_tactic.all_goals t
 
-meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : smt_tactic unit :=
-slift (tactic.interactive.induction p rec_name ids)
+meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
+  (revert : parse $ (tk "generalizing" *> ident*)?) : smt_tactic unit :=
+slift (tactic.interactive.induction p rec_name ids revert)
 
 open tactic
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 19f420668b..a8263deb2c 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"match", 0}, {"^.", g_max_prec+1},
-         {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
+         {"renaming", 0}, {"extends", 0}, {"generalizing", 0}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "axioms", "variable", "protected", "private",