X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=6c6ef2b50f2089230f39eabd50db0bccbaee0736;hb=0ad07ee93a134773c16986552dc88e4e50a437ce;hp=711a1527d940c17fdb66b2c0acabc85c5eb1d967;hpb=4f2e7eacea9e8b3089a575d7bf529fd5e70e8453;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 711a1527d..6c6ef2b50 100644
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -34,17 +34,12 @@ type coercion_search_result =
   | 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
+  | NotHandled
 
 val look_for_coercion :
   Cic.metasenv -> Cic.substitution -> Cic.context ->
    Cic.term -> Cic.term -> coercion_search_result
 
-val look_for_coercion' :
-  Cic.metasenv -> Cic.substitution -> Cic.context ->
-   CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
-
 (* checks if term is a constant or 
  * a constant applyed that is marked with (`Class `Coercion) *)
 val is_composite: Cic.term -> bool
@@ -54,12 +49,12 @@ 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
+val coerced_arg: Cic.term list -> (Cic.term * int) 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 -> 
+  bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr -> 
     (CoercDb.coerc_carr * Cic.metasenv * 
       (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list