1. More debugging code

[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 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