From d29e538e11bc1d703baa7cbcdeca160f7627dc90 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 27 Apr 2006 10:06:54 +0000 Subject: [PATCH] Added is_trans_eq_URI and is_sym_eq_URI --- helm/software/components/cic/libraryObjects.ml | 4 ++++ helm/software/components/cic/libraryObjects.mli | 2 ++ 2 files changed, 6 insertions(+) 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;; -- 2.39.2