diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-03 20:33:26 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-03 20:33:57 +0100 |
| commit | 424c69af24c11453c4835aa30f0602f93d1eb775 (patch) | |
| tree | 1cc01e5bbf45310c8901575f0cdb8abe052735f2 /src/common/Vericertlib.v | |
| parent | d312521d80f41bd7901d7b8b3617e75b3a35f8b3 (diff) | |
| download | vericert-424c69af24c11453c4835aa30f0602f93d1eb775.tar.gz vericert-424c69af24c11453c4835aa30f0602f93d1eb775.zip | |
Add lemmas relating to new HTLgen operations
Diffstat (limited to 'src/common/Vericertlib.v')
| -rw-r--r-- | src/common/Vericertlib.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index ae63e25..6437612 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -57,9 +57,9 @@ 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 := +Ltac auto_apply H := match goal with - | H' : _ |- _ => solve [ apply H in H'; auto | auto ] + | H' : _ |- _ => apply H in H' end. (** Specialize all hypotheses with a forall to a specific term *) |