Pantograph/Frontend/Elab.lean

@@ -122,13 +122,6 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
 protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
   t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
 
-protected def usedConstants (t: TacticInvocation) : NameSet :=
-  let info := t.info
-  info.goalsBefore
-    |>.filterMap info.mctxAfter.getExprAssignmentCore?
-    |>.map Expr.getUsedConstantsAsSet
-    |>.foldl .union .empty
-
 end TacticInvocation
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@@ -165,13 +158,7 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
     let tactic ← invocation.ctx.runMetaM {} do
       let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
       return t.pretty
-    let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
-    return {
-      goalBefore,
-      goalAfter,
-      tactic,
-      usedConstants,
-    }
+    return { goalBefore, goalAfter, tactic }
 
 structure InfoWithContext where
   info: Elab.Info

Pantograph/Protocol.lean

@@ -298,9 +298,6 @@ structure InvokedTactic where
   goalBefore: String
   goalAfter: String
   tactic: String
-
-  -- List of used constants
-  usedConstants: Array String
   deriving Lean.ToJson
 
 structure CompilationUnit where

Test/Integration.lean

@@ -167,8 +167,8 @@ example : ∀ (p: Prop), p → p := by
 
 def test_frontend_process : Test :=
   [
-    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
-    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
+    let file := "example : ∀ (p: Prop), p → p := by\n  intro p h\n  exact h"
+    let goal1 := "p : Prop\nh : p\n⊢ p"
     step "frontend.process"
       [
         ("file", .str file),
@@ -180,16 +180,14 @@ def test_frontend_process : Test :=
          boundary := (0, file.utf8ByteSize),
          invocations? := .some [
            {
-             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
+             goalBefore := "⊢ ∀ (p : Prop), p → p",
              goalAfter := goal1,
-             tactic := "intro p q h",
-             usedConstants := #[],
+             tactic := "intro p h",
            },
            {
              goalBefore := goal1 ,
              goalAfter := "",
-             tactic := "exact Or.inl h",
-             usedConstants := #["Or.inl"],
+             tactic := "exact h",
            },
          ]
        }],