Skip to content

Commit

Permalink
change Admitted to Abort for exnc
Browse files Browse the repository at this point in the history
  • Loading branch information
@palmskog
palmskog committed Nov 20, 2018
1 parent 2aac56a commit b9a21a0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/noaliasBT.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,4 +157,4 @@ split.
(* just as it should *)
rewrite !(negbTE (noaliasR D)).
admit.
Admitted.
Abort.

2 comments on commit b9a21a0

@palmskog
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@anton-trunov this is the last Admitted we have. I compared this to the corresponding example in noaliasCTC.v, and they have the same final proof state before the last admit. However, that example ends with Abort. I think it's safe to say this was never meant to be Qedd (premise doesn't even mention x4). Do you agree?

@anton-trunov
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@palmskog Sure, there is no doubt.

Please sign in to comment.