From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 27 Apr 2006 10:06:54 +0000 (+0000)
Subject: Added is_trans_eq_URI and is_sym_eq_URI
X-Git-Tag: make_still_working~7391
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d29e538e11bc1d703baa7cbcdeca160f7627dc90;p=helm.git

Added is_trans_eq_URI and is_sym_eq_URI
---

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
diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli
index eca5a0d90..db15cdff8 100644
--- a/helm/software/components/cic/libraryObjects.mli
+++ b/helm/software/components/cic/libraryObjects.mli
@@ -31,6 +31,8 @@ val eq_URI : unit -> UriManager.uri
 val is_eq_URI : UriManager.uri -> bool
 val is_eq_ind_URI : UriManager.uri -> bool
 val is_eq_ind_r_URI : UriManager.uri -> bool
+val is_trans_eq_URI : UriManager.uri -> bool
+val is_sym_eq_URI : UriManager.uri -> bool
 
 exception NotRecognized;;