- let t = CicUtil.term_of_uri uri in
- let ty, _ =
- CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
- in
- (uri, t, ty)::l)
- []
- (let t1 = Unix.gettimeofday () in
- let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
- let t2 = Unix.gettimeofday () in
- (debug_print
- (lazy
- (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
- (t2 -. t1))));
- eqs)
- in
- let eq_uri1 = eq_XURI ()
- and eq_uri2 = LibraryObjects.eq_URI () in
- let iseq uri =
- (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)