Closed briangmilnes closed 1 year ago
You have to explicitly ask F to reload dependences. F does dependency scanning when the file is opened, and if you add a dependence on a module after the file is opened, then you have to ask F* to scan it for deps again.
The F* menu, Proof State sub menu, has an option for this (or use C-c C-r)
If you create a file Foo.fst
and enter and validate a module Foo line (c-c c-n) then enter an open FStar.Mul it can't find the module.
You have to save and reopen the file.
Odd