- commit completed :)

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

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index 0fd2b8cba221a4844dc0bb255632f1133bf108f1..18ec015df87e2b1c55dbdb4faf7fe792ad1b775d 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -37,8 +37,12 @@ let message2 m1 t1 m2 t2 =
 let error2 err m1 t1 m2 t2 =
    err (message2 m1 t1 m2 t2)
 
+let zero = Some 0
+
+let one = Some 1
+
 let assert_convertibility err f st m u t =
-   if BR.are_convertible st m (Some 0) u m (Some 1) t then f () else
+   if BR.are_convertible st m zero u m one t then f () else
    error2 err m u m t
 
 let assert_applicability err f st m v t =
@@ -46,7 +50,7 @@ let assert_applicability err f st m v t =
       | _, B.Sort _                      ->
          error1 err "not a function" m t
       | mw, B.Bind (_, B.Abst (_, w), _) ->
-         if BR.are_convertible st mw (Some 0) w m (Some 1) v then f () else
+         if BR.are_convertible st mw zero w m one v then f () else
         error2 err mw w m v
       | _                                -> assert false (**)