X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.mli;h=711a1527d940c17fdb66b2c0acabc85c5eb1d967;hb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;hp=ae2bd9233943c3d1993be89f0c05d1fb6a775396;hpb=e5bcf92808b75387ef4d4ff0f827bf07ad9af2f7;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index ae2bd9233..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