X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagType.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagType.ml;h=4f447276b3f71a4fb529d04883604be4c7106792;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=9069040115e3eb1e3a43c4728a6f45abf67abd53;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml
index 906904011..4f447276b 100644
--- a/helm/software/lambda-delta/src/basic_ag/bagType.ml
+++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml
@@ -54,16 +54,14 @@ let rec b_type_of f st c x =
    | Z.Sort h                    ->
       let h = H.apply h in f x (Z.Sort h) 
    | Z.LRef i                    ->
-      let f = function
-         | Some (_, Z.Abst w)               -> f x w
-	 | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w
-	 | Some (_, Z.Abbr _)               -> assert false
-	 | Some (_, Z.Void)                 -> 
-	    error1 "reference to excluded variable" c x
-         | None                             ->
-	    error1 "variable not found" c x	 
+      let err () = error1 "variable not found" c x in
+      let f _ = function
+         | Z.Abst w               -> f x w
+	 | Z.Abbr (Z.Cast (w, v)) -> f x w
+	 | Z.Abbr _               -> assert false
+	 | Z.Void                 -> error1 "reference to excluded variable" c x	 
       in
-      Z.get f c i
+      Z.get err f c i
    | Z.GRef uri                  ->
       let f = function
          | _, _, E.Abst (_, w)          -> f x w
@@ -72,30 +70,30 @@ let rec b_type_of f st c x =
 	 | _, _, E.Void                 -> assert false
       in
       ZE.get_entity f uri   
-   | Z.Bind (l, id, Z.Abbr v, t) ->
+   | Z.Bind (a, l, Z.Abbr v, t) ->
       let f xv xt tt =
-         f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt)
+         f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
       in
       let f xv cc = b_type_of (f xv) st cc t in
-      let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in
+      let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
       let f xv vv = match xv with 
 	 | Z.Cast _ -> f xv
          | _        -> f (Z.Cast (vv, xv))
       in
       type_of f st c v
-   | Z.Bind (l, id, Z.Abst u, t) ->
+   | Z.Bind (a, l, Z.Abst u, t) ->
       let f xu xt tt =
-	 f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt)
+	 f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
       in
       let f xu cc = b_type_of (f xu) st cc t in
-      let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in
+      let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
       type_of f st c u
-   | Z.Bind (l, id, Z.Void, t)   ->
+   | Z.Bind (a, l, Z.Void, t)   ->
       let f xt tt = 
-         f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt)
+         f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
       in
       let f cc = b_type_of f st cc t in
-      Z.push "type void" f c l id Z.Void   
+      Z.push "type void" f c a l Z.Void   
    | Z.Appl (v, t)            ->
       let f xv vv xt tt = function
 	 | ZR.Abst w                             ->