From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 May 2006 08:22:10 +0000 (+0000)
Subject: better exception
X-Git-Tag: 0.4.95@7852~1466
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3077a8a3657bba79d3edad3fb483122ea3126b72;p=helm.git

better exception
---

diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml
index e1c9e1396..223b24edd 100644
--- a/components/cic/libraryObjects.ml
+++ b/components/cic/libraryObjects.ml
@@ -53,7 +53,7 @@ let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
 
 (**** SET_DEFAULT ****)
 
-exception NotRecognized;;
+exception NotRecognized of string;;
 
 (* insert an element in front of the list, removing from the list all the
    previous elements with the same key associated *)
@@ -76,7 +76,7 @@ let set_default what l =
       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
   | "absurd",[absurd_URI] ->
       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
-  | _,_ -> raise NotRecognized
+  | _,_ -> raise (NotRecognized what)
 
 let reset_defaults () =
   eq_URIs_ref := default_eq_URIs;
@@ -96,7 +96,7 @@ 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 =
+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
@@ -104,22 +104,22 @@ let is_sym_eq_URI uri =
 let sym_eq_URI ~eq:uri =
  try
   let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let trans_eq_URI ~eq:uri =
  try
   let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_URI ~eq:uri =
  try
   let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_r_URI ~eq:uri =
  try
   let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let true_URI () = List.hd !true_URIs_ref
 let false_URI () = List.hd !false_URIs_ref
diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli
index db15cdff8..1fa0dcc83 100644
--- a/components/cic/libraryObjects.mli
+++ b/components/cic/libraryObjects.mli
@@ -34,7 +34,7 @@ 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;;
+exception NotRecognized of string;;
 
 val eq_ind_URI : eq:UriManager.uri -> UriManager.uri
 val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri