ignoreUsableFacts option bug fix

leanprover-community · Oct 15, 2024 · e68416d · e68416d
1 parent a0afb1e
commit e68416d
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
@@ -67,7 +67,8 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
   match stx with
   | `($id:ident) =>
     let some expr ← Term.resolveId? id
-      | throwError "Unknown identifier {id}"
+      | if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Unknown identifier {id}"
     match expr with
     | .const exprConstName _ =>
       match (← getEnv).find? exprConstName with