From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 27 Nov 2006 13:48:35 +0000 (+0000)
Subject: Added in_eq_uris.
X-Git-Tag: 0.4.95@7852~771
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d4775af99f2a2c4a0e7fc7f5cde32a08af4a592;p=helm.git

Added in_eq_uris.
---

diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml
index dc36636fe..d8af91a6f 100644
--- a/components/cic/libraryObjects.ml
+++ b/components/cic/libraryObjects.ml
@@ -79,8 +79,8 @@ let reset_defaults () =
   false_URIs_ref := default_false_URIs;
   absurd_URIs_ref := default_absurd_URIs
 
-(**** LOOKUP FUNCTIONS ****)
 
+(**** LOOKUP FUNCTIONS ****)
 let eq_URI () =
  try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
  with Failure "hd" -> None
@@ -96,7 +96,6 @@ let is_eq_refl_URI uri =
 
 let is_eq_ind_URI uri =
  List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
-
 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 = 
@@ -108,6 +107,11 @@ let is_eq_f_URI uri =
 let is_eq_f_sym_URI uri =
  List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 
+let in_eq_URIs uri =  
+  is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri || 
+  is_eq_ind_r_URI uri || is_trans_eq_URI uri || is_sym_eq_URI uri || 
+  is_eq_f_URI uri || is_eq_f_sym_URI uri
+
 
  
 let eq_refl_URI ~eq:uri =
diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli
index 0cd9f2e97..0bf8bfea5 100644
--- a/components/cic/libraryObjects.mli
+++ b/components/cic/libraryObjects.mli
@@ -26,6 +26,7 @@
 val set_default : string -> UriManager.uri list -> unit
 val reset_defaults : unit -> unit 
 
+
 val eq_URI : unit -> UriManager.uri option
 
 val is_eq_URI : UriManager.uri -> bool
@@ -36,6 +37,7 @@ val is_trans_eq_URI : UriManager.uri -> bool
 val is_sym_eq_URI : UriManager.uri -> bool
 val is_eq_f_URI : UriManager.uri -> bool
 val is_eq_f_sym_URI : UriManager.uri -> bool
+val in_eq_URIs : UriManager.uri -> bool
 
 val eq_URI_of_eq_f_URI : UriManager.uri -> UriManager.uri