Commit 7d393c2b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Let done do eassumption.

parent d800f42e
...@@ -44,6 +44,7 @@ Ltac done := ...@@ -44,6 +44,7 @@ Ltac done :=
[ repeat first [ repeat first
[ solve [trivial] [ solve [trivial]
| solve [symmetry; trivial] | solve [symmetry; trivial]
| eassumption
| reflexivity | reflexivity
| discriminate | discriminate
| contradiction | contradiction
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment