X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=44f30d278a00f69792788d3a074754804f509421;hb=a22628e5de37d3ffe9de056d7683f2ebdf7226fb;hp=6c6ef2b50f2089230f39eabd50db0bccbaee0736;hpb=0ad07ee93a134773c16986552dc88e4e50a437ce;p=helm.git diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index 6c6ef2b50..44f30d278 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -40,13 +40,9 @@ val look_for_coercion : Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term -> Cic.term -> 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 +val generate_dot_file: Format.formatter -> unit (* given the Appl contents returns the argument of the head coercion *) val coerced_arg: Cic.term list -> (Cic.term * int) option