X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=36c114d8f8f85fff695a01040ec3185e83934247;hb=9b09890767aaa93e512324f8e7f13e2cdeebac88;hp=5fe0f35a5b549e74414e16d2c26abce830c50523;hpb=1b9751de891efa2761cdc6cb9d019df6aaaa8514;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 5fe0f35a5..36c114d8f 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -620,12 +620,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
 (*DEBUGGING ONLY:
 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 *)
-                     let inner_coerced t =
+                     let inner_coerced ?(skip_non_c=false) t =
                       let t = CicMetaSubst.apply_subst subst t in
                       let rec aux c x t =
                         match t with
                         | Cic.Appl l -> 
                             (match CoercGraph.coerced_arg l with
+                            | None when skip_non_c -> 
+                                aux c (HExtlib.list_last l)            
+                                 (HExtlib.list_last l)            
                             | None -> c, x
                             | Some (t,_) -> aux (List.hd l) t t)
                         | _ ->  c, x
@@ -712,17 +715,19 @@ res)
                                 metasenv l1 l2 ugraph
                          | _ -> raise exn
                       else
-                       let grow1 =
-                         match last_tl1 with Cic.Meta _ -> true | _ -> false in
-                       let grow2 =
-                         match last_tl2 with Cic.Meta _ -> true | _ -> false in
-                       if not (grow1 || grow2) then
-                          (* no flexible terminals -> no pullback, but
-                           * we still unify them, in some cases it helps *)
-                          conclude subst metasenv ugraph last_tl1 last_tl2
-                       else
+                      let grow1 =
+                        match last_tl1 with Cic.Meta _ -> true | _ -> false in
+                      let grow2 =
+                        match last_tl2 with Cic.Meta _ -> true | _ -> false in
+                      if not (grow1 || grow2) then
+                        let _,last_tl1 = 
+                          inner_coerced ~skip_non_c:true (Cic.Appl l1) in 
+                        let _,last_tl2 = 
+                          inner_coerced ~skip_non_c:true  (Cic.Appl l2) in
+                        conclude subst metasenv ugraph last_tl1 last_tl2
+                      else
                         let meets = 
-                          CoercGraph.meets 
+                           CoercGraph.meets 
                             metasenv subst context (grow1,car1) (grow2,car2)
                         in
                         (match meets with