Local opens

Similarly to the OCaml let open construct, we have:

module L = FStar.List

let example1 =
  let open L in
  rev (append [] [])

let example2 =
  L (rev (append [] []))

The latter is sugar for the former. Please note that the latter form is slightly different from the OCaml syntax, which would be: L.(rev (append [] [])).

Bug: you cannot do

open FStar

let example3 =
  List (rev (append [] []))

this is a bug and should be fixed.