diff options
Diffstat (limited to 'src/common/Vericertlib.v')
| -rw-r--r-- | src/common/Vericertlib.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |