Avoid confusion for names of proofs put in the applicative context.

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

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 91d10242d6469bf4f09f81701a5b30c2c9109585..912ae1e8e0cbbee2d4deba85595418032c9ce04b 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -628,51 +628,44 @@ let res =
                              metasenv (C.Appl l1) (C.Appl l2) ugraph
                          | _ -> raise exn)
                       else
-                       let meets = CoercGraph.meets car1 car2 in
+                       let meets = 
+                         CoercGraph.meets metasenv subst context car1 car2 
+                       in
                         (match meets with
                         | [] -> 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] -> 
+                        | (carr,metasenv,to1,to2)::xxx -> 
+                          (match xxx with
+                          [] -> ()
+                          | (m2,_,c2,c2')::_ ->
+                          let m1,_,c1,c1' = carr,metasenv,to1,to2 in
+                          let unopt = 
+                            function Some (_,t) -> CicPp.ppterm t 
+                            | None -> "id"
+                          in
+                          HLog.warn 
+                            ("There are two minimal joins of "^
+                            CoercDb.name_of_carr car1^" and "^
+                            CoercDb.name_of_carr car2^": " ^ 
+                            CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
+                            unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+                            unopt c2^" + "^unopt c2'));
                           let last_tl1',(subst,metasenv,ugraph) =
-                           match last_tl1 with
-                            | Cic.Meta (i1,l1)
-                              when not (CoercDb.eq_carr m car1) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car1
-                                with
-                                 | CoercGraph.SomeCoercion [metasenv,last,coerced]
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl1,to1 with
+                            | Cic.Meta (i1,l1),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl1 ugraph
-                                 | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl1,(subst,metasenv,ugraph) in
+                            | _ -> last_tl1,(subst,metasenv,ugraph) 
+                          in
                           let last_tl2',(subst,metasenv,ugraph) =
-                           match last_tl2 with
-                              Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car2
-                                with
-                                   (*CSC: bu here: I am considering only the first one*)
-                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl2,to2 with
+                            | Cic.Meta (i2,l2),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl2 ugraph
-                                 | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl2,(subst,metasenv,ugraph)
+                            | _ -> last_tl2,(subst,metasenv,ugraph) 
                           in
-(*DEBUGGING ONLY:
+                        (*DEBUGGING ONLY:
 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 *)
                            let subst,metasenv,ugraph =