From d5385a8cbab840438cab0e59b5bbbd51e471ee73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 23:00:23 +0100
Subject: [PATCH] Obligation Tactic is already idtac.
---
theories/typing/sum.v | 2 --
1 file changed, 2 deletions(-)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 9f53f4c1..3fadde0b 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -7,8 +7,6 @@ Set Default Proof Using "Type".
Section sum.
Context `{typeG Σ}.
- Local Obligation Tactic := idtac.
-
Program Definition emp : type :=
{| ty_size := 1%nat;
ty_own tid vl := False%I;
--
GitLab