Interleaving misses (and therefore keeps) pragmas at the tail of the file

[mtzguido]

trafficstars

Yet another reason to remove interleaving. A.fsti:

module A

#push-options "--z3rlimit 40 --admit_smt_queries true"

val lem (x:int) : Lemma True

#pop-options

A.fst:

module A
let lem (x:int) = ()

Checking the interface works. Checking the implementation gives:

* Error 65 at A.fsti(7,0-7,12):
  - Cannot #pop-options, stack would become empty                                                                                                                                                                                                                                                                                                     

1 error was reported (see above)  

[mtzguido]

Gah, I thought this was just an easy fix of filtering them, but that means breaking the uint modules which have

 #set-options "--lax"
 //This private primitive is used internally by the
 //compiler to translate bounded integer constants
 //with a desugaring-time check of the size of the number,
 //rather than an expensive verification check.
 //Since it is marked private, client programs cannot call it directly
 //Since it is marked unfold, it eagerly reduces,
 //eliminating the verification overhead of the wrapper
 private
 unfold
 let __uint_to_t (x:int) : Tot t
     = uint_to_t x
 #reset-options

at the end of the file (the interleaved decl in the fst would fail). I won't fix this right now.