chore: fix test

This commit is contained in:
Leonardo de Moura 2022-10-27 18:57:25 -07:00
parent 25beba6624
commit 31d2c8fb66

View file

@ -6,13 +6,13 @@
skip
trivial
[Elab.step.result] ?m
[Elab.step]
skip
trivial
[Elab.step]
skip
trivial
[Elab.step] skip
[Elab.step]
skip
trivial
[Elab.step]
skip
trivial
[Elab.step] trivial
[Elab.step] (apply And.intro✝) <;> trivial
[Elab.step] focus