X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2Fbag.ml;fp=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2Fbag.ml;h=51c644148a55a5a4671da2e6a5b85e4f67efb16e;hb=fec20705af4705f8eb9542aece87769b82a6a6b4;hp=c0e540963e45e26d2b8056da38863b34277f292b;hpb=b37863d4598516a06241f18ad0db963399015bf2;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml
index c0e540963..51c644148 100644
--- a/helm/software/helena/src/basic_ag/bag.ml
+++ b/helm/software/helena/src/basic_ag/bag.ml
@@ -16,22 +16,22 @@ module P = Marks
 module E = Entity
 
 type uri = E.uri
-type attrs = E.node_attrs
+type b_attrs = E.bind_attrs
 
 type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
           | Abbr of term (* abbreviation *)
 
-and term = Sort of int                          (* hierarchy index *)
-         | LRef of P.mark                       (* location *)
-         | GRef of uri                          (* reference *)
-         | Cast of term * term                  (* domain, element *)
-         | Appl of term * term                  (* argument, function *)
-         | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *)
+and term = Sort of int                            (* hierarchy index *)
+         | LRef of P.mark                         (* location *)
+         | GRef of uri                            (* reference *)
+         | Cast of term * term                    (* domain, element *)
+         | Appl of term * term                    (* argument, function *)
+         | Bind of b_attrs * P.mark * bind * term (* name, location, binder, scope *)
 
 type entity = term E.entity (* attrs, uri, binder *)
 
-type lenv = (attrs * P.mark * bind) list (* name, location, binder *) 
+type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *) 
 
 type message = (lenv, term) Log.item list
 
@@ -47,24 +47,24 @@ let cast u t = Cast (u, t)
 
 let appl u t = Appl (u, t)
 
-let bind a l b t = Bind (a, l, b, t)
+let bind y l b t = Bind (y, l, b, t)
 
-let bind_abst a l u t = Bind (a, l, Abst u, t)
+let bind_abst y l u t = Bind (y, l, Abst u, t)
 
-let bind_abbr a l v t = Bind (a, l, Abbr v, t)
+let bind_abbr y l v t = Bind (y, l, Abbr v, t)
 
 (* local environment handling functions *************************************)
 
 let empty_lenv = []
 
-let push msg f es a l b =
+let push msg f es y l b =
    let rec does_not_occur loc = function
       | []                          -> true
       | (_, l, _) :: _ when l = loc -> false
       | _ :: es                     -> does_not_occur l es
    in
    if not (does_not_occur l es) then failwith msg else
-   let c = (a, l, b) :: es in f c
+   let c = (y, l, b) :: es in f c
 
 let append f es1 es2 = 
    f (List.append es2 es1)
@@ -77,7 +77,7 @@ let contents f es = f es
 let get err f es i =
    let rec aux = function
       | []              -> err ()
-      | (a, l, b) :: tl -> if l = i then f a b else aux tl
+      | (y, l, b) :: tl -> if l = i then f y b else aux tl
    in
    aux es