X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=e1c9e1396bef4f5c5efc19cab6885bda0038c5de;hb=f7f2a793b445a052138cd3df377a9e417f6e37c4;hp=adbc219cc3fd72771b314a3e61eeea85a98cfc52;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index adbc219cc..e1c9e1396 100644 --- 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