the commit contnues by updating the RTM and modifying the typechecker accordingly

[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 f23da87d09fad4304838ccff99d8c5420756b5ae..9dcce08a6781d51f6a1471713ffc887fcfd73efd 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -21,8 +21,6 @@ module BE = BrgEnvironment
 module BS = BrgSubstitution
 module BR = BrgReduction
 
-type message = (BR.kam, B.term) Log.message
-
 (* Internal functions *******************************************************)
 
 let level = 4
@@ -51,15 +49,15 @@ let error3 err m t1 t2 ?mu t3 =
    err (message3 m t1 t2 ?mu t3)
 
 let assert_convertibility err f st m u w v =
-   if BR.are_convertible st m u m w then f () else
+   if BR.are_convertible st m (Some 0) u m (Some 0) w then f () else
    error3 err m v w u
 
 let assert_applicability err f st m u w v =
-   match BR.xwhd st m u with 
+   match BR.xwhd st m None u with 
       | _, B.Sort _                      ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (_, u), _) -> 
-         if BR.are_convertible st mu u m w then f () else
+         if BR.are_convertible st mu (Some 0) u m (Some 0) w then f () else
         error3 err m v w ~mu u
       | _                                -> assert false (**)