* choice from the user is needed to disambiguate the term
* @raise Ambiguous_term for ambiguous term *)
val disambiguate_string:
* choice from the user is needed to disambiguate the term
* @raise Ambiguous_term for ambiguous term *)
val disambiguate_string:
Helm_registry.load_from !configuration_file;
ignore (CicNotation2.load_notation [] core_notation_script);
ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
Helm_registry.load_from !configuration_file;
ignore (CicNotation2.load_notation [] core_notation_script);
ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")