1. The last commit that fixed unification of compound coercions with

[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 8deb6af4aed58807d89cc79d82e052ae7cdb08f1..d1e010ca696558aefe36f8b2ec95f334634aea16 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -575,7 +575,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                 fo_unif_l 
                   test_equality_only subst metasenv (lr1, lr2)  ugraph
               with 
-              | UnificationFailure _ as exn -> 
+              | UnificationFailure _
+              | Uncertain _ as exn -> 
                   (match l1, l2 with
                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
@@ -583,7 +584,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                     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
+                        | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
                         | _ -> assert false
                       in
                       let body2, attrs2, ugraph =