]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgType.ml
Code simplified.
[helm.git] / helm / software / lambda-delta / basic_rg / brgType.ml
index cf997e473e0ac7fb02e0565cec13a1ebe88cefaa..a35a9c32afe3ca657bd381a1586c359cc3d5f40b 100644 (file)
@@ -14,6 +14,7 @@ module C = Cps
 module A = Share
 module L = Log
 module H = Hierarchy
+module Y = Entity
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
@@ -82,14 +83,12 @@ let rec b_type_of err f ~si g m x =
       R.get err f m i
    | B.GRef (_, uri)           ->
       let f = function
-         | _, _, B.Abst (_, w)                -> f x w
-        | _, _, B.Abbr (_, B.Cast (_, w, _)) -> f x w
-        | _, _, B.Abbr _                     -> assert false
-        | _, _, B.Void _                     ->
-           error1 err "reference to excluded entry" m x
+         | _, _, Y.Abst w                  -> f x w
+        | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
+        | _, _, Y.Abbr _                  -> assert false
       in
       let err _ = error1 err "reference to unknown entry" m x in
-      E.get_entry err f uri   
+      E.get_entity err f uri   
    | B.Bind (B.Abbr (a, v), t) ->
       let f xv xt tt =
          f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)