chore: missing profileitM

leanprover · Jul 15, 2024 · 32d60c5 · 32d60c5
1 parent 57b8b32
commit 32d60c5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -52,7 +52,8 @@ private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNa
   | Except.error msg      => throwError msg
   | Except.ok levelParams => pure levelParams
 
-def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
+def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) :=
+do profileitM Exception s!"fix level params" (← getOptions) do
   -- We used to use `shareCommon` here, but is was a bottleneck
   let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
   let us := levelParams.map mkLevelParam

diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
@@ -153,7 +153,7 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
     preDef.termination.decreasingBy?.isSome
 
 
-def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
+def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do profileitM Exception "add pre-definitions" (← getOptions) do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef