From: Claudio Sacerdoti Coen Date: Tue, 2 Jan 2007 19:00:34 +0000 (+0000) Subject: 1. More debugging code X-Git-Tag: make_still_working~6550 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=094ad6d3aa96472adb6614f0f21f4cbdf94ad0bc;hp=1c95887fc7af68023b8b682a34816d8fb4d0a716;p=helm.git 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 bcae08df8..91d10242d 100644 --- 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