diff --git a/editor/code/views/info/Goals.tsx b/editor/code/views/info/Goals.tsx
index 531b77da..4cfc33b9 100644
--- a/editor/code/views/info/Goals.tsx
+++ b/editor/code/views/info/Goals.tsx
@@ -61,16 +61,24 @@ function Goal({ goal, idx, open }: GoalP) {
     }
   });
 
+  // XXX: We want to add an option for this that can be set interactively
+  let show_goal_on_header = false;
+
+  let gtyp = (
+    <div style={{ marginLeft: "1ex" }} className={className} ref={tyRef}>
+      <CoqPp content={goal.ty} inline={false} />
+    </div>
+  );
+
   return (
     <div className="coq-goal-env" ref={ref}>
       <Details summary={`Goal (${idx})`} open={open}>
         <div style={{ paddingTop: "1ex" }} />
         <Hyps hyps={goal.hyps} />
         <hr />
+        {show_goal_on_header ? "" : gtyp}
       </Details>
-      <div style={{ marginLeft: "1ex" }} className={className} ref={tyRef}>
-        <CoqPp content={goal.ty} inline={false} />
-      </div>
+      {show_goal_on_header ? gtyp : ""}
     </div>
   );
 }