- method disambiguateTermAst ?(context = []) ?(metasenv = []) ?(env = _env)
- termAst
- =
- match disambiguate_term mqiconn context metasenv termAst ~aliases:env with
- | [ x ] -> x
+ method chooseUris = !_chooseUris
+ method setChooseUris f = _chooseUris := f
+
+ method chooseInterp = !_chooseInterp
+ method setChooseInterp f = _chooseInterp := f
+
+ val parserr = parserr_instance ()
+ method parserr = parserr
+
+ val dbd = MatitaMisc.dbd_instance ()
+
+ method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst =
+ let (save_state, env) =
+ match env with
+ | Some env -> (false, env)
+ | None -> (true, _env)
+ in
+ match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph
+ ~dbd context metasenv termAst ~aliases:env with
+ | [ (env, metasenv, term,ugraph) as x ] ->
+ if save_state then self#setEnv env;
+ x