X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgType.ml;h=a35a9c32afe3ca657bd381a1586c359cc3d5f40b;hb=f00757144b2cd7e6457fed55dbc1309d11a542dc;hp=cf997e473e0ac7fb02e0565cec13a1ebe88cefaa;hpb=79684e8bd0f54b5c88fff981366bd8c78dd0fbe9;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index cf997e473..a35a9c32a 100644
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -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)