diff --git a/docs/data.ipynb b/docs/data.ipynb
index 4c09b4d..f3afbc0 100644
--- a/docs/data.ipynb
+++ b/docs/data.ipynb
@@ -117,83 +117,83 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "=== Before ===\n",
+      "[Before]\n",
       "α : Sort ?u.7\n",
       "⊢ α → α\n",
-      "===Tactic===\n",
-      "aesop\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "aesop (using [])\n",
+      "[Afte]\n",
       "\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
-      "===Tactic===\n",
-      "intro p q h\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "intro p q h (using [])\n",
+      "[Afte]\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "cases h\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "cases h (using ['Eq.refl', 'Or'])\n",
+      "[Afte]\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
       "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "apply Or.inr\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "apply Or.inr (using ['Or.inr'])\n",
+      "[Afte]\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
-      "===Tactic===\n",
-      "assumption\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "assumption (using [])\n",
+      "[Afte]\n",
       "\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inr\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "apply Or.inl\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "apply Or.inl (using ['Or.inl'])\n",
+      "[Afte]\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
-      "===Tactic===\n",
-      "assumption\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "assumption (using [])\n",
+      "[Afte]\n",
       "\n"
      ]
     }
    ],
    "source": [
     "for i in invocations:\n",
-    "    print(f\"=== Before ===\\n{i.before}\")\n",
-    "    print(f\"===Tactic===\\n{i.tactic}\")\n",
-    "    print(f\"===After===\\n{i.after}\")"
+    "    print(f\"[Before]\\n{i.before}\")\n",
+    "    print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
+    "    print(f\"[Afte]\\n{i.after}\")"
    ]
   },
   {
diff --git a/pantograph/compiler.py b/pantograph/compiler.py
index e881cec..38469bf 100644
--- a/pantograph/compiler.py
+++ b/pantograph/compiler.py
@@ -9,9 +9,13 @@ class TacticInvocation:
     before: str
     after: str
     tactic: str
+    used_constants: list[str]
 
     @staticmethod
     def parse(payload: dict):
-        return TacticInvocation(before=payload["goalBefore"],
-                                after=payload["goalAfter"],
-                                tactic=payload["tactic"])
+        return TacticInvocation(
+            before=payload["goalBefore"],
+            after=payload["goalAfter"],
+            tactic=payload["tactic"],
+            used_constants=payload.get('usedConstants', []),
+        )
diff --git a/src b/src
index 8fe4c78..4f6ccd3 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 8fe4c78c2aea194869bb7b4b7e61087b6374ff66
+Subproject commit 4f6ccd3e82dd41402b7244484a1b0312d9e27018