fixed undo support for coercions inside records

[helm.git] / helm / ocaml / library / coercDb.ml

diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml
index bc3d2a745d8d77a247718781b1671e0e52571c91..ac5067585b9c0d5b4cb6409de9f9e77f57bd18d9 100644 (file)
--- 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
+  
+
+