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

[helm.git] / helm / software / components / cic_unification / cicUnification.ml

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 91d10242d6469bf4f09f81701a5b30c2c9109585..a7a3a16741e50889b1a60a823eb41cd6d6f7452f 100644 (file)
--- 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