X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=711a1527d940c17fdb66b2c0acabc85c5eb1d967;hb=6ca04b596642894449012de8ec6d2f3f784f5868;hp=62e4844997e72f73bc02ae8e0c99fecaaee7f264;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 62e484499..711a1527d 100644
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -32,6 +32,7 @@ type coercion_search_result =
      (* to apply the coercion it is sufficient to unify the last coercion
         argument (that is a Meta) with the term to be coerced *)
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+  | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
@@ -52,7 +53,13 @@ val source_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
 
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> Cic.term option
+
+(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
 val meets : 
+  Cic.metasenv -> Cic.substitution -> Cic.context ->
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> 
-    CoercDb.coerc_carr list
+    (CoercDb.coerc_carr * Cic.metasenv * 
+      (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list