Case c1 t1 vs c2 t2 where c1 and c2 are not splitted and t1 and t2

are rigid was not handled correctly. Fixed.

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 54e7fc5f25bd9cfdadd9f01582a25d941ccd4755..5fe0f35a5b549e74414e16d2c26abce830c50523 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -659,6 +659,31 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl
                               (Cic.Appl (bo::args))
                         | _ -> assert false
                       in
+                      let conclude subst metasenv ugraph last_tl1' last_tl2' =
+                       let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline 
+  ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
+   " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+                        fo_unif_subst test_equality_only subst context
+                         metasenv last_tl1' last_tl2' ugraph
+                       in
+                       if subst = subst' then raise exn 
+                       else
+(*DEBUGGING ONLY:
+let subst,metasenv,ugrph as res = 
+*)
+                        fo_unif_subst test_equality_only subst' context
+                         metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline 
+  (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+   " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+                      in
                       if CoercDb.eq_carr car1 car2 then
                          match last_tl1,last_tl2 with
                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
@@ -671,44 +696,22 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl
                             fo_unif_subst test_equality_only subst context
                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
                          | _ when CoercDb.eq_carr head1_c head2_c ->
-                           let l1, l2 = 
                              (* composite VS composition + metas avoiding
                               * coercions not only in coerced position    *)
-                             if c1 = cc1 then 
-                               unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
-                             else if c2 = cc2 then
-                               Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
-                             else raise exn
-                           in
-                            fo_unif_subst test_equality_only subst context
-                             metasenv l1 l2 ugraph
+                             if c1 <> cc1 && c2 <> cc2 then
+                               conclude subst metasenv ugraph
+                                last_tl1 last_tl2
+                             else
+                              let l1, l2 = 
+                               if c1 = cc1 then 
+                                 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+                               else
+                                 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                              in
+                               fo_unif_subst test_equality_only subst context
+                                metasenv l1 l2 ugraph
                          | _ -> raise exn
                       else
-                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
-                        let subst',metasenv,ugraph =
-(*DEBUGGING ONLY:
-prerr_endline 
-  ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
-   " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
-*)
-                         fo_unif_subst test_equality_only subst context
-                          metasenv last_tl1' last_tl2' ugraph
-                        in
-                        if subst = subst' then raise exn 
-                        else
-(*DEBUGGING ONLY:
-let subst,metasenv,ugraph as res = 
-*)
-                         fo_unif_subst test_equality_only subst' context
-                          metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
-in
-(prerr_endline 
-  (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
-   " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-res)
-*)
-                       in
                        let grow1 =
                          match last_tl1 with Cic.Meta _ -> true | _ -> false in
                        let grow2 =