+ if restricted_univ = [] then
+ let ct =
+ if use_context then find_context_theorems context metasenv else []
+ in
+ let lt =
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
+ let cache = AutoCache.cache_empty in
+ let cache = cache_add_list cache context (ct@lt) in
+ let tables =
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ List.fold_left
+ (fun (a,p,b) (t,ty) ->
+ let mes = CicUtil.metas_of_term ty in
+ Saturation.add_to_active b a p env ty t
+ (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
+ automation_cache.AutomationCache.tables ct
+ in
+(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables =
+ * tables }; *)
+ automation_cache.AutomationCache.univ, tables, cache
+ else
+ let metasenv, t_ty, s_t_ty, _ =
+ List.fold_left
+ (fun (metasenv,acc, sacc, maxmeta) t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ let head, metasenv, args, maxmeta =
+ TermUtil.saturate_term maxmeta metasenv context ty 0
+ in
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
+ (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
+ in
+ let automation_cache = AutomationCache.empty () in
+ let automation_cache =
+ let universe = automation_cache.AutomationCache.univ in
+ let universe =
+ Universe.index_list universe context t_ty
+ in
+ { automation_cache with AutomationCache.univ = universe }
+ in
+ let automation_cache =
+ List.fold_left
+ (fun c (t,ty) ->
+ AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
+ automation_cache s_t_ty
+ in
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_add_list cache_empty context t_ty
+;;
+ (*
+(* let signature = MetadataQuery.signature_of metasenv goal in *)
+(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)