]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/library/coercGraph.mli
Warning Y fixed.
[helm.git] / helm / ocaml / library / coercGraph.mli
index fcbed3497313fd840b81d36000d5e3eef7d3dd6a..1923a964a7fa8e799fe890194232d696c3af34c1 100644 (file)
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* This module implements the Query interface to the Coercion Graph *)
+
 type coercion_search_result = 
   | SomeCoercion of Cic.term
   | NoCoercion
@@ -32,8 +34,7 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
-(* also adds them to the Db *)
-val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
-    (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+val is_a_coercion: Cic.term -> bool
+val source_of: Cic.term -> Cic.term
+val target_of: Cic.term -> Cic.term