1. More debugging code

2. "Bug" "fixed": when the pullback of two coercions is computed, only the
   join is returned, but not the two coercions that complete the pullback.
   Thus we need to recompute them and it may happen that we find more than one
   parallel coercions. This "fix" just randomly picks the first one (instead
   of raising an assert false). All this stuff must be handled in a better way.

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index bcae08df80e69cafa21de0e5e695fa83ff737eb7..91d10242d6469bf4f09f81701a5b30c2c9109585 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -633,6 +633,8 @@ let res =
                         | [] -> raise exn
                         | _::_::_ ->
 prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
+let m1::m2::_ = meets in
+prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
 assert false
                         | [m] -> 
                           let last_tl1',(subst,metasenv,ugraph) =
@@ -659,7 +661,8 @@ assert false)
                                  CoercGraph.look_for_coercion' metasenv subst
                                   context m car2
                                 with
-                                 | CoercGraph.SomeCoercion [metasenv,last,coerced]
+                                   (*CSC: bu here: I am considering only the first one*)
+                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
                                    ->
                                     last,
                                     fo_unif_subst test_equality_only subst context