fix cc tactic

leanprover-community · Sep 6, 2024 · dfbd837 · dfbd837
1 parent 39b0689
commit dfbd837
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/Mathlib/Tactic/CC/Addition.lean b/Mathlib/Tactic/CC/Addition.lean
@@ -1470,7 +1470,8 @@ partial def propagateEqUp (e : Expr) : CCM Unit := do
     if ← isInterpretedValue ra <&&> isInterpretedValue rb <&&>
         pure (ra.int?.isNone || ra.int? != rb.int?) then
       raNeRb := some
-        (Expr.app (.proj ``Iff 0 (← mkAppM ``bne_iff_ne #[ra, rb])) (← mkEqRefl (.const ``true [])))
+        (Expr.app (.proj ``Iff 0 (← mkAppOptM ``bne_iff_ne #[none, none, none, ra, rb]))
+          (← mkEqRefl (.const ``true [])))
     else
       if let some c₁ ← isConstructorApp? ra then
       if let some c₂ ← isConstructorApp? rb then
@@ -1808,7 +1809,8 @@ def propagateValueInconsistency (e₁ e₂ : Expr) : CCM Unit := do
   let some eqProof ← getEqProof e₁ e₂ | failure
   let trueEqFalse ← mkEq (.const ``True []) (.const ``False [])
   let neProof :=
-    Expr.app (.proj ``Iff 0 (← mkAppM ``bne_iff_ne #[e₁, e₂])) (← mkEqRefl (.const ``true []))
+    Expr.app (.proj ``Iff 0 (← mkAppOptM ``bne_iff_ne #[none, none, none, e₁, e₂]))
+      (← mkEqRefl (.const ``true []))
   let H ← mkAbsurd trueEqFalse eqProof neProof
   pushEq (.const ``True []) (.const ``False []) H