X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=3bc6273c34e44721dcf76ea85bfb0e16e3171db9;hb=dc1902ae1e458e5120af63d880dbd08255bef238;hp=1a3be89f38efb20bc13b77b3752d232b4c8992b7;hpb=910c252965fe17d6b5af92e4658e7d02bac82d58;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 1a3be89f3..3bc6273c3 100644
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -40,14 +40,6 @@ 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
-
 val source_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
@@ -58,7 +50,7 @@ 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