* choice from the user is needed to disambiguate the term
* @raise Ambiguous_term for ambiguous term *)
val disambiguate_string:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?context:Cic.context ->
?metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
in
try
- fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+ fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ("",0,ast)
?initial_ugraph ~aliases ~universe:None)
with Exit -> raise (Ambiguous_term (lazy term))
end
let core_notation_script = "../../../matita/core_notation.moo";;
-let get_from_user ~(dbd:HMysql.dbd) =
+let get_from_user ~(dbd:HSql.dbd) =
let rec get () =
match read_line () with
| "" -> []
Helm_registry.load_from !configuration_file;
ignore (CicNotation2.load_notation [] core_notation_script);
ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
- let dbd = HMysql.quick_connect
+ let dbd = HSql.quick_connect
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")