From 56f442f41aba4efb3929b79f15e5a4cc87579acb Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Thu, 12 Aug 2021 20:24:14 +0100
Subject: Complete HTLspec (mostly)

---
 src/common/Vericertlib.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/common')

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 0fae032..84c272b 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -218,7 +218,9 @@ Ltac liapp :=
          | _ => idtac
          end.
 
-Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
+Ltac plia := solve [ unfold Ple in *; lia ].
+
+Ltac crush := simplify; try discriminate; try congruence; try plia; liapp;
               try assumption; try (solve [auto]).
 
 Ltac crush_trans :=
-- 
cgit