diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-08 17:43:35 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-08 17:43:45 +0100 |
| commit | 12a8b9d3cf31b35dcaff13b9e7c2d38fbf432403 (patch) | |
| tree | 6ebb952af2b3af4a64bf1882ae007bc46365a56c /src/common | |
| parent | 8fa89c3e400fff4e9a4ec28eba6393cdca48362b (diff) | |
| download | vericert-12a8b9d3cf31b35dcaff13b9e7c2d38fbf432403.tar.gz vericert-12a8b9d3cf31b35dcaff13b9e7c2d38fbf432403.zip | |
Progress on tr_module proof
Diffstat (limited to 'src/common')
| -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. |