]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brg.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_rg / brg.ml
index c9b5ee41573edfaa56f9a6cd7384ace307aab9d6..eeb9f56d61bdb00ae4d2aab5b0bfa5216659566d 100644 (file)
@@ -16,7 +16,7 @@ module E = Entity
 module N = Level
 
 type uri = E.uri
-type attrs = E.attrs
+type attrs = E.node_attrs
 
 type bind = Void                   (*             *)
           | Abst of N.level * term (* level, type *)
@@ -62,7 +62,7 @@ let empty = Null
 let push e c a b = Cons (e, c, a, b)
 
 let rec get i = function
-   | Null                         -> Null, Null, [], Void
+   | Null                         -> Null, Null, E.empty_node, Void
    | Cons (e, c, a, b) when i = 0 -> e, c, a, b
    | Cons (e, _, _, _)            -> get (pred i) e