+let equations_for_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ match main with
+ None -> raise Goal_is_not_an_equation
+ | Some (m,l) ->
+ if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then
+ let set = signature_of_hypothesis context in
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let set = close_with_types set metasenv context in
+ let set = close_with_constructors set metasenv context in
+ let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+ else raise Goal_is_not_an_equation
+