X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=d1e010ca696558aefe36f8b2ec95f334634aea16;hb=ec13ac23f555f04b0a546d0e8ae464d9b5806d9b;hp=8deb6af4aed58807d89cc79d82e052ae7cdb08f1;hpb=83bbd662d887cc43d7d60cb607295dce503b3b7f;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 8deb6af4a..d1e010ca6 100644
--- 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 =