val debug_parse_only : Debug.flagval debug_type_only : Debug.flagval open_file : Env.env -> Env.pathname -> unitval close_file : unit -> Pmodule.pmodule Wstdlib.Mstr.tval open_module : Ptree.ident -> unitval close_module : Loc.position -> unitval open_scope : Loc.position -> Ptree.ident -> unitval close_scope : Loc.position -> import:bool -> unitval import_scope : Loc.position -> Ptree.qualid -> unitval add_decl : Loc.position -> Ptree.decl -> unitval string_list_of_qualid : Ptree.qualid -> string listval print_qualid : Format.formatter -> Ptree.qualid -> unitval type_term_in_namespace :
Theory.namespace ->
Decl.known_map ->
Coercion.t ->
Ptree.term ->
Term.termval type_fmla_in_namespace :
Theory.namespace ->
Decl.known_map ->
Coercion.t ->
Ptree.term ->
Term.term