]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgValidity.ml
- simpler attribute system
[helm.git] / helm / software / helena / src / basic_rg / brgValidity.ml
index c616b22df68c023eedc60257548cc96d9279a446..5de70fbfa5cd70172495e51c325bc18ce42cd8ac 100644 (file)
@@ -83,18 +83,18 @@ let rec b_validate err f st m y =
         | _, _, _, E.Void   ->
             error1 err "reference to unknown entry" m y
       end
-   | B.Bind (a, b, t) ->
-      let f () = b_validate err f st (BR.push m a b) t in
+   | B.Bind (y, b, t) ->
+      let f () = b_validate err f st (BR.push m y b) t in
       begin match b with 
          | B.Abst (_, n, u) -> validate err f st m u
          | B.Abbr v         -> validate err f st m v
          | B.Void           -> f ()
       end
-   | B.Appl (_, x, v, t)    ->
+   | B.Appl (x, v, t)       ->
       let f () = assert_applicability err f st m x v t in
       let f () = b_validate err f st m t in
       validate err f st m v
-   | B.Cast (_, u, t)        ->
+   | B.Cast (u, t)          ->
       let f () = assert_convertibility err f st m u t in
       let f () = b_validate err f st m t in
       validate err f st m u