pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Change some tactics to use their usual names in the book code

Browse source
This commit is contained in:
Adam Chlipala 2016-03-13 21:15:03 -04:00
parent 8f0c986a00
commit 0fe16514a4
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
LambdaCalculusAndTypeSoundness.v
View file

@ -928,9 +928,9 @@ Module Stlc.
* scope of the book. *)
Ltac t0 := match goal with
| [ H : ex _ |- _ ] => destruct H
| [ H : _ /\ _ |- _ ] => destruct H
| [ |- context[?x ==v ?y] ] => destruct (x ==v y)
| [ H : ex _ |- _ ] => invert H
| [ H : _ /\ _ |- _ ] => invert H
| [ |- context[?x ==v ?y] ] => cases (x ==v y)
| [ H : Some _ = Some _ |- _ ] => invert H
| [ H : step _ _ |- _ ] => invert H
@ -940,7 +940,7 @@ Module Stlc.
| [ H : plug _ _ _ |- _ ] => invert1 H
end; subst.
Ltac t := simplify; propositional; repeat (t0; simplify); try congruence; eauto 6.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
Lemma progress_snazzy : forall e t,
hasty $0 e t