+let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
+ let (_, metasenv, _, _) = proof in
+ let add_uris_for acc goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ let set = signature_of_hypothesis context metasenv in
+ let set =
+ match main with
+ None -> set
+ | Some (main,l) ->
+ List.fold_right Constr.UriManagerSet.add (main::l) set in
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let all_constants_closed = close_with_types set metasenv context in
+ Constr.UriManagerSet.union all_constants_closed acc
+ in
+ let all_constants_closed =
+ List.fold_left add_uris_for Constr.UriManagerSet.empty goals in
+ (* we split predicates from the rest *)
+ let predicates, rest =
+ Constr.UriManagerSet.partition is_predicate all_constants_closed
+ in
+ prerr_endline ("FOO!1");
+ let uris =
+ Constr.UriManagerSet.fold
+ (fun u acc ->
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,[]),all_constants_closed)
+ in
+ acc @ uris)
+ predicates []
+ in
+ prerr_endline ("FOO!2");
+(*
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed)
+ in
+*)
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ let uris = List.filter (only all_constants_closed) uris in
+ uris
+;;
+
+let filter_out_predicate set ctx menv =
+ Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
+;;
+
+let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+ let to_string set =
+ "{\n" ^
+ (String.concat "\n"