X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=6c6ef2b50f2089230f39eabd50db0bccbaee0736;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=abc94688c5a6b27897ca1c63b2fc8a1946e45efd;hpb=70211a10f741fe77945f5a720596df2b686f344d;p=helm.git diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index abc94688c..6c6ef2b50 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -54,7 +54,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