feat: open in terms and tatics

See #330

src/Lean/Elab/Tactic/Basic.lean

@@ -305,8 +305,10 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
 @[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx =>
   focus $ evalTactic stx[1]
 
--- @[builtinTactic Lean.Parser.Tactic.«open»] def evalOpen : Tactic := fun stx =>
---   focus $ evalTactic stx[1]
+@[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
+  let openDecls ← elabOpenDecl stx[1]
+  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+    evalTactic stx[3]
 
 @[builtinTactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let gs ← getUnsolvedGoals

src/Lean/Elab/Term.lean

@@ -1424,12 +1424,10 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
   | some msg => elabTermEnsuringType stx[2] expectedType? true msg
 
-/- Uncomment after update stage0
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
   let openDecls ← elabOpenDecl stx[1]
   withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
     elabTerm stx[3] expectedType?
--/
 
 private def mkSomeContext : Context := {
   fileName      := "<TermElabM>"

tests/lean/run/openTermTactic.lean

@@ -0,0 +1,37 @@
+def f (x : Nat) :=
+  open Nat in
+  succ (succ x)
+
+theorem f_eq : f x = Nat.succ (Nat.succ x) :=
+  rfl
+
+def g (x : Nat) := open Nat in succ (succ x)
+
+theorem f_eq_g : f x = g x := rfl
+
+def h (x : Nat) := Nat.succ (open Nat in succ x)
+
+theorem f_eq_h : f x = h x := rfl
+
+open Nat in
+def h' (x : Nat) := succ x
+
+theorem ex (x y : Nat) (h : x = y) : x + 1 = y + 1 := by
+  open Nat in show succ x = succ y
+  apply congrArg
+  assumption
+
+
+inductive InductiveWithAVeryLongName where
+  | c1 | c2 | c3 | c4 | c5 | c6 | c7
+
+def foo (e : InductiveWithAVeryLongName) : Type :=
+  open InductiveWithAVeryLongName in
+  match e with
+    | c1 => Nat
+    | c2 => Nat → Nat
+    | c3 => Nat → Nat → Nat
+    | c4 => Nat → Nat → Nat → Nat
+    | c5 => Nat → Nat → Nat → Nat → Nat
+    | c6 => Nat → Nat → Nat → Nat → Nat → Nat
+    | c7 => Nat → Nat → Nat → Nat → Nat → Nat → Nat