A failing unification of a coercion vs a term is now tried again after

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

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index b1ef27f4ec9399e83cb9e2d366e97810f7f4e8ec..8deb6af4aed58807d89cc79d82e052ae7cdb08f1 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -571,8 +571,57 @@ 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 _ 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