X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=7a4112ad5a67350a9110b54d1cc4516fd848a451;hb=50844b0116c863862434c7c673c5caaf6ff78cdf;hp=df653eb9a7ab3657d59d97691a5de2e3407ba532;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index df653eb9a..7a4112ad5 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -82,6 +82,12 @@ let eq_URI () =
 let is_eq_URI uri =
  List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
 
+let is_eq_refl_URI uri =
+  let urieq = UriManager.strip_xpointer uri in
+  is_eq_URI urieq &&
+  not (UriManager.eq urieq uri)
+;;
+
 let is_eq_ind_URI uri =
  List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
 
@@ -92,6 +98,10 @@ let is_trans_eq_URI uri =
 let is_sym_eq_URI uri =
  List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 
+let eq_refl_URI ~eq:uri =
+  let uri = UriManager.strip_xpointer uri in
+  UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
+ 
 let sym_eq_URI ~eq:uri =
  try
   let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x