_kenji_toplevel

Top level declarations are being extracted to ocaml code and this has the following implications:

1. Cannot be ghost since it will just correspond to a term without computation content and will be implemented as assert false.
2. Right now, cannot be anything except Tot (which is added implicitly if needed) since it is unsound, for example:

let rec f (x: unit) : Dv False = f x                                                                                                          
let g: False = f ()

It produces a warning but type check successfully because it is used in mitls carefully in order to allocate global references like is common in ocaml.