Bugs fixed:

[helm.git] / helm / software / components / cic / libraryObjects.ml

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index adbc219cc3fd72771b314a3e61eeea85a98cfc52..e1c9e1396bef4f5c5efc19cab6885bda0038c5de 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -96,6 +96,10 @@ let is_eq_ind_URI uri =
 
 let is_eq_ind_r_URI uri =
  List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
+let is_trans_eq_URI uri =
+ List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
+let is_sym_eq_URI uri =
+ List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 
 let sym_eq_URI ~eq:uri =
  try