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

diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml
index 5e7c07b5b..51c644148 100644
--- a/helm/software/helena/src/basic_ag/bag.ml
+++ b/helm/software/helena/src/basic_ag/bag.ml
@@ -12,25 +12,26 @@
 (* kernel version: basic, absolute, global *)
 (* note          : experimental *) 
 
+module P = Marks
 module E = Entity
 
 type uri = E.uri
-type attrs = E.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 int                       (* location *)
-         | GRef of uri                       (* reference *)
-         | Cast of term * term               (* domain, element *)
-         | Appl of term * term               (* argument, function *)
-         | Bind of attrs * int * 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 * int * bind) list (* name, location, binder *) 
+type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *) 
 
 type message = (lenv, term) Log.item list
 
@@ -46,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)
@@ -76,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