From 7d393c2bd78922152b8a8db6216bd3f6e152f058 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 11:35:49 +0100
Subject: [PATCH] Let done do eassumption.
---
prelude/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 843644e83..e12aef1be 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -44,6 +44,7 @@ Ltac done :=
[ repeat first
[ solve [trivial]
| solve [symmetry; trivial]
+ | eassumption
| reflexivity
| discriminate
| contradiction
--
GitLab