From b2eeb3e69eca87a41b204daa9fb924447cbbc365 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 15:30:41 +0100
Subject: [PATCH] Remove unused f_lia tactics.

---
 prelude/tactics.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index e12aef1be..665b96f63 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -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
-- 
GitLab