- commit completed :)

[helm.git] / helm / software / helena / src / basic_rg / brgType.ml

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 9dcce08a6781d51f6a1471713ffc887fcfd73efd..7c47ff12cd10df8dcd36b266f5a3df39153e20d7 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -48,8 +48,10 @@ let message3 m t1 t2 ?mu t3 =
 let error3 err m t1 t2 ?mu t3 =
    err (message3 m t1 t2 ?mu t3)
 
+let zero = Some 0
+
 let assert_convertibility err f st m u w v =
-   if BR.are_convertible st m (Some 0) u m (Some 0) w then f () else
+   if BR.are_convertible st m zero u m zero w then f () else
    error3 err m v w u
 
 let assert_applicability err f st m u w v =
@@ -57,7 +59,7 @@ let assert_applicability err f st m u w v =
       | _, B.Sort _                      ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (_, u), _) -> 
-         if BR.are_convertible st mu (Some 0) u m (Some 0) w then f () else
+         if BR.are_convertible st mu zero u m zero w then f () else
         error3 err m v w ~mu u
       | _                                -> assert false (**)