Skip to content
Snippets Groups Projects
Commit d5385a8c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Obligation Tactic is already idtac.

parent 6bf9591c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 2 deletions
theories/typing/sum.v
+ 0
− 2
View file @ d5385a8c
...@@ -7,8 +7,6 @@ Set Default Proof Using "Type". ...@@ -7,8 +7,6 @@ Set Default Proof Using "Type".
Section sum. Section sum.
Context `{typeG Σ}. Context `{typeG Σ}.
Local Obligation Tactic := idtac.
Program Definition emp : type := Program Definition emp : type :=
{| ty_size := 1%nat; {| ty_size := 1%nat;
ty_own tid vl := False%I; ty_own tid vl := False%I;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment