From 2d4775af99f2a2c4a0e7fc7f5cde32a08af4a592 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 13:48:35 +0000 Subject: [PATCH] Added in_eq_uris. --- components/cic/libraryObjects.ml | 8 ++++++-- components/cic/libraryObjects.mli | 2 ++ 2 files changed, 8 insertions(+), 2 deletions(-) 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 -- 2.39.2