fix

leanprover-community · Jan 14, 2025 · b1378c9 · b1378c9
1 parent a9c19df
commit b1378c9
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
@@ -63,8 +63,8 @@ def kind : Info → String
   | .ofCustomInfo         _ => "CustomInfo"
   | .ofFVarAliasInfo      _ => "FVarAliasInfo"
   | .ofFieldRedeclInfo    _ => "FieldRedeclInfo"
-  | .ofOmissionInfo       _ => "OmissionInfo"
   | .ofChoiceInfo         _ => "ChoiceInfo"
+  | .ofDelabTermInfo      _ => "DelabTermInfo"
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 def stx? : Info → Option Syntax
@@ -80,8 +80,8 @@ def stx? : Info → Option Syntax
   | .ofCustomInfo         info => info.stx
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
   | .ofChoiceInfo         info => info.stx
+  | .ofDelabTermInfo      info => info.stx
 
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 def isOriginal (i : Info) : Bool :=