Fix option setting removal

[JasonGross]

In order to efficiently manipulate the file, I have to break it into definitions. I will now attempt to do this. Sending statements to coqtop... Done. Splitting to definitions... Warning: found multiple timing info in 'Chars 78290 - 78364 [Set~Warnings~"-funind-cannot-b...] 0. secs (0.u,0.s)\nChars 78381 - 78389 [Defined.] 0.06 secs (0.06u,0.s)\n\nCoq < 2119 || 0 < ': [('78290', '78364'), ('78381', '78389')]

Non-fatal error: Failed to split file to definitions and preserve the error.
The new error was: Warning: Cannot open /Users/bcpierce/tmp/VST/compcert [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/msl [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/sepcomp [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/veric [cannot-open-path,filesystem] Warning: Cannot open /Users/bcpierce/tmp/VST/floyd [cannot-open-path,filesystem] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 520, characters 30-42: Warning: Notation Lt.lt_irrefl is deprecated since 8.16. The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead. [deprecated-syntactic-definition,deprecated] File "/tmp/tmp74xmcokl/VC/EverythingVCRequires.v", line 4996, characters 0-1: Error: Syntax error: illegal begin of vernac.

Split not saved. Splitting to definitions with options settings failed, skipping useless option settings removal Sending statements to coqtop... Done. Splitting to definitions... Warning: found multiple timing info in 'Chars 62435 - 62509 [Set~Warnings~"-funind-cannot-b...] 0. secs (0.u,0.s)\nChars 62511 - 62519 [Defined.] 0.059 secs (0.059u,0.s)\n\nCoq < 1061 || 0 < ': [('62435', '62509'), ('62511', '62519')]

Presumably the code inserts option settings in the middle of proofs is bugging out or something