From 675147dcfcab75bb0826e73c7e749a31a93768ca Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Wed, 1 Jun 2022 09:53:43 -0400
Subject: [PATCH] fix: make InteractiveHyp.fvarIds optional

This is for backwards compat.
---
 src/Lean/Widget/InteractiveGoal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 556abe4d1c..49d13199b5 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -14,7 +14,7 @@ open Server
 
 structure InteractiveHypothesis where
   names : Array String
-  fvarIds : Array FVarId
+  fvarIds? : Option (Array FVarId)
   type : CodeWithInfos
   val? : Option CodeWithInfos := none
   isInstance : Bool