Commit 1331d75b authored by Robbert Krebbers's avatar Robbert Krebbers

Remove unused f_lia tactics.

parent 85a4e1af
......@@ -204,13 +204,6 @@ Ltac simplify_equality := repeat
end.
Ltac simplify_equality' := repeat (progress csimpl in * || simplify_equality).
Ltac f_equal' := csimpl in *; f_equal.
Ltac f_lia :=
repeat lazymatch goal with
| |- @eq BinNums.Z _ _ => lia
| |- @eq nat _ _ => lia
| |- _ => f_equal
end.
Ltac f_lia' := csimpl in *; f_lia.
Ltac setoid_subst_aux R x :=
match goal with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment