From 73b2693b1b743b0f5ee677a37ae47311dde71694 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.
---
theories/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/tactics.v b/theories/tactics.v
index aee81d73..0d2cabaf 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -44,6 +44,7 @@ Ltac done :=
[ repeat first
[ solve [trivial]
| solve [symmetry; trivial]
+ | eassumption
| reflexivity
| discriminate
| contradiction
--
GitLab