diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-02 11:12:45 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-02 11:12:45 +0100 |
| commit | 564fb33a504d7611d73bbe5e20b23453e141ed3d (patch) | |
| tree | 441cd64ddf97c3288693a1041904a8a502715754 /src/common | |
| parent | b8107dbffc3c9a27b7beb4014883a55102389a29 (diff) | |
| download | vericert-564fb33a504d7611d73bbe5e20b23453e141ed3d.tar.gz vericert-564fb33a504d7611d73bbe5e20b23453e141ed3d.zip | |
Simplify some HTLgenspec proofs
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Vericertlib.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index c537cef..722edef 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -57,6 +57,11 @@ Ltac learn_tac fact name := Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name. Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name. +Ltac auto_hyp H := + match goal with + | H' : _ |- _ => solve [ apply H in H'; auto | auto ] + end. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := |