cleanup

src/Lean/Elab/MutualDef.lean

@@ -64,8 +64,6 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
     throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
   if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
     throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
-  if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then
-    throwError "'noncomputable unsafe' is not allowed"
   if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
     throwError "'noncomputable partial' is not allowed"
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
@@ -769,8 +767,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
     let kind ← if kind.isDefOrAbbrevOrOpaque then
-    -- Convert any proof let recs inside a `def` to `theorem` kind
-          withLCtx c.toLift.lctx c.toLift.localInstances do
+      -- Convert any proof let recs inside a `def` to `theorem` kind
+      withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind
     else if kind.isTheorem then
       -- Convert any non-proof let recs inside a `theorem` to `def` kind

src/Lean/Elab/SyntheticMVars.lean

@@ -288,20 +288,6 @@ private def processPostponedUniverseContraints : TermElabM Unit := do
 private def markAsResolved (mvarId : MVarId) : TermElabM Unit :=
   modify fun s => { s with syntheticMVars := s.syntheticMVars.erase mvarId }
 
-/-
-def withNarrowedReuse [Monad m] [MonadExceptOf Exception m] (modify : Option (Language.SyntaxGuardedSnapshotBundle Tactic.TacticParsedSnapshot))
-    (parse : Syntax → Option (Syntax × TSyntax inner)) (act : TSyntax inner → m α) : Syntax → m α :=
-  fun stx => do
-    let some (outer, inner) := parse stx
-      | throwUnsupportedSyntax
-    withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
-      { tacSnap with old? := tacSnap.old?.bind fun old => do
-        let (oldOuter, oldInner) ← parse old.stx
-        guard <| outer.structRangeEq oldOuter
-        return { old with stx := oldInner }
-      }
-    }) (act inner)-/
-
 mutual
 
   /--

src/Lean/Elab/Tactic/Basic.lean

@@ -98,7 +98,7 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : TacticM Unit :=
 
 /--
 Restores full state including sources for unique identifiers. Only intended for incremental reuse
-betweeen elaboration runs, not for backtracking within a single run.
+between elaboration runs, not for backtracking within a single run.
 -/
 def SavedState.restoreFull (b : SavedState) : TacticM Unit := do
   b.term.restoreFull

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -182,9 +182,11 @@ def addCheckpoints (stx : Syntax) : TacticM Syntax := do
   output := output ++ currentCheckpointBlock
   return stx.setArgs output
 
+builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq1Indented
 @[builtin_tactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
   Term.withNarrowedArgTacticReuse (argIdx := 0) evalSepTactics
 
+builtin_initialize registerBuiltinIncrementalTactic ``tacticSeqBracketed
 @[builtin_tactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do
   let initInfo ← mkInitialTacticInfo stx[0]
   withRef stx[2] <| closeUsingOrAdmit do
@@ -271,6 +273,7 @@ private def getOptRotation (stx : Syntax) : Nat :=
     throwError "failed on all goals"
   setGoals mvarIdsNew.toList
 
+builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq
 @[builtin_tactic tacticSeq] def evalTacticSeq : Tactic :=
   Term.withNarrowedArgTacticReuse (argIdx := 0) evalTactic