X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=d1e010ca696558aefe36f8b2ec95f334634aea16;hb=82ec52f9e431b17659033cbfdcaa56c44d9e285d;hp=b1ef27f4ec9399e83cb9e2d366e97810f7f4e8ec;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index b1ef27f4e..d1e010ca6 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -571,8 +571,58 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         fo_unif_l 
                           test_equality_only subst' metasenv' (l1,l2) ugraph1
               in
+              (try 
                 fo_unif_l 
-                  test_equality_only subst metasenv (lr1, lr2)  ugraph)
+                  test_equality_only subst metasenv (lr1, lr2)  ugraph
+              with 
+              | UnificationFailure _
+              | Uncertain _ as exn -> 
+                  (match l1, l2 with
+                  | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
+                     (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
+                    CoercGraph.is_a_coercion c1 && 
+                    CoercGraph.is_a_coercion c2 ->
+                      let body1, attrs1, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri1 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
+                        | _ -> assert false
+                      in
+                      let body2, attrs2, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri2 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+                        | _ -> assert false
+                      in
+                      let is_composite1 = 
+                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                      let is_composite2 = 
+                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                      (match is_composite1, is_composite2 with
+                      | false, false -> raise exn
+                      | true, false ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl = Cic.Appl (body1::tl1) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                              redappl t2 ugraph
+                      | false, true -> 
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl = Cic.Appl (body2::tl2) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             t1 redappl ugraph
+                      | true, true ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl1 = Cic.Appl (body1::tl1) in
+                          let redappl1 = CicReduction.head_beta_reduce appl1 in
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl2 = Cic.Appl (body2::tl2) in
+                          let redappl2 = CicReduction.head_beta_reduce appl2 in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             redappl1 redappl2 ugraph)
+                  | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2