*)
val find_library_equalities:
HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
- UriManager.UriSet.t * equality list * int
+ UriManager.UriSet.t * (UriManager.uri * equality) list * int
(**
searches the library for theorems that are not equalities (returned by the
*)
val equality_of_term: Cic.term -> Cic.term -> equality
+(**
+ Re-builds the term corresponding to this equality
+*)
+val term_of_equality: equality -> Cic.term
+
val term_is_equality: Cic.term -> bool
(** tests a sort of alpha-convertibility between the two terms, but on the