- let environment',metasenv,expr =
- Disambiguate'.disambiguate_term mqi_handle context metasenv
- (input#buffer#get_text ()) !environment
+ let environment',metasenv,expr,ugraph =
+ match
+ Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+ (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph
+ ~aliases:!environment
+ with
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
+ | _ -> assert false