X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercDb.ml;h=bc3d2a745d8d77a247718781b1671e0e52571c91;hb=5dd5b3f6cd990d4d126b44c092e1df7f86c506d4;hp=437ad65ae202bcddab717c3fa5e5d327f63d6dfc;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git

diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml
index 437ad65ae..bc3d2a745 100644
--- a/helm/ocaml/library/coercDb.ml
+++ b/helm/ocaml/library/coercDb.ml
@@ -28,7 +28,6 @@ exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 
 let db = ref []
-let use_coercions = ref true
 
 let coerc_carr_of_term t =
   try
@@ -69,7 +68,14 @@ let remove_coercion p =
   db := List.filter (fun u -> not(p u)) !db
 
 let find_coercion f =
-  if !use_coercions then
-    List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
-  else []
+  List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+
+let is_a_coercion u =
+  List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+
+let get_carr uri =
+  try
+    let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+    src, tgt
+  with Not_found -> assert false (* uri must be a coercion *)