diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 9f53f4c187e1318dfa3385a90ff4cfeeb4aae12b..3fadde0b8ca447a3f30833177927a510ff8edc57 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;