Skip to content
Snippets Groups Projects
Commit b2eeb3e6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove unused f_lia tactics.

parent 886b7737
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment