X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercDb.ml;h=ac5067585b9c0d5b4cb6409de9f9e77f57bd18d9;hb=f4f050696e66b8604d9f0ff8173afe03addf74d6;hp=bc3d2a745d8d77a247718781b1671e0e52571c91;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml
index bc3d2a745..ac5067585 100644
--- a/helm/ocaml/library/coercDb.ml
+++ b/helm/ocaml/library/coercDb.ml
@@ -79,3 +79,10 @@ let get_carr uri =
     src, tgt
   with Not_found -> assert false (* uri must be a coercion *)
 
+let term_of_carr = function
+  | Uri u -> CicUtil.term_of_uri u
+  | Sort s -> Cic.Sort s
+  | Term _ -> assert false
+  
+
+