module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks)
-let mqi_debug_fun = ignore
-let mqi_flags = []
-
-let parse ?(uri_pred = constants_only) =
- let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun in
+let parse mqi_handle ?(uri_pred = constants_only) =
uri_predicate := uri_pred;
let empty_environment =
DisambiguatingParser.EnvironmentP3.of_string
Disambiguate'.disambiguate_term
mqi_handle empty_context empty_metasenv input empty_environment
in
- MQIConn.close mqi_handle; (metasenv, term)
+ (metasenv, term)
-let parse_pp ?uri_pred input = CicPp.ppterm (snd (parse ?uri_pred input))
+let parse_pp mqi_handle ?uri_pred input =
+ CicPp.ppterm (snd (parse mqi_handle ?uri_pred input))