X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=a7a3a16741e50889b1a60a823eb41cd6d6f7452f;hb=31614ae3b2c3260d381c77643e87ab683b347b58;hp=91d10242d6469bf4f09f81701a5b30c2c9109585;hpb=094ad6d3aa96472adb6614f0f21f4cbdf94ad0bc;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 91d10242d..a7a3a1674 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -645,7 +645,7 @@ assert false
                                  CoercGraph.look_for_coercion' metasenv subst
                                   context m car1
                                 with
-                                 | CoercGraph.SomeCoercion [metasenv,last,coerced]
+                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
                                    ->
                                     last,
                                     fo_unif_subst test_equality_only subst context