From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 2 Jan 2007 19:03:33 +0000 (+0000)
Subject: Same fix of the previous commit, but in a different case.
X-Git-Tag: make_still_working~6549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=31614ae3b2c3260d381c77643e87ab683b347b58;p=helm.git

Same fix of the previous commit, but in a different case.
---

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