From 12a8b9d3cf31b35dcaff13b9e7c2d38fbf432403 Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Sat, 8 May 2021 17:43:35 +0100
Subject: Progress on tr_module proof

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

(limited to 'src/common/Vericertlib.v')

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 48edd08..ef4a10b 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -216,6 +216,8 @@ Ltac crush_trans :=
   | [ H : ?inter = ?g |- _ = ?g ] => transitivity inter; crush
   end.
 
+Ltac maybe t := t + idtac.
+
 Global Opaque Nat.div.
 Global Opaque Z.mul.
 
-- 
cgit