Problems opening a module that was previously imported under a given name

[jberthold-ms]

When a module is first imported under a given name, like

module L = FStar.List.Tot

the compiler issues a warning if the module is then opened under the given name:

open L

* Warning 285 at ModuleOpen.fst(13,5-13,6):
  - No modules in namespace L and no file with that name either

Despite the warning, the bindings in L are subsequently in scope so the open actually worked, it just causes the warning to be printed.

Full example code:

module ModuleOpen

let test_data: list int = [1; 2; 3]

module L = FStar.List.Tot

let test1 = List.Tot.map (fun x -> x + 1) test_data

let test2 = L.map (fun x -> x + 1) test_data

let _ = assert ( test2 = test1)

open L
(* 
* Warning 285 at ModuleOpen.fst(13,5-13,6):
  - No modules in namespace L and no file with that name either
*)
(* But this nevertheless works, `map` is now in scope from L *)
let test3 = map (fun x -> x + 1) test_data
(* without `open L`: 
* Error 72 at ModuleOpen.fst(19,12-19,15):
  - Identifier not found: [map]
*)

let _ = assert ( test3 = test2)