obj
end
-module Trivial =
-struct
- exception Ambiguous_term of string Lazy.t
- exception Exit
- module Callbacks =
- struct
- let interactive_user_uri_choice ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- raise Exit
- let interactive_interpretation_choice interp = raise Exit
- let input_or_locate_uri ~(title:string) ?id = raise Exit
- end
- module Disambiguator = Make (Callbacks)
- let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
- ?(aliases = DisambiguateTypes.Environment.empty) term
- =
- let ast =
- CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
- in
- try
- fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
- ?initial_ugraph ~aliases ~universe:None)
- with Exit -> raise (Ambiguous_term (lazy term))
-end
-