]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgEnvironment.ml
update in delayed_updating
[helm.git] / helm / software / helena / src / basic_rg / brgEnvironment.ml
index 1b3f744e2b43a3469ed04deb4814dba32b073a7c..01a38f89ffeffa52e296b023b3816d083f0389f0 100644 (file)
@@ -21,9 +21,14 @@ let env = UH.create hsize
 
 (* decps *)
 let set_entity entity =
+IFDEF EXPAND THEN
    let ra, na, uri, b = entity in
-   let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in
+   let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in
    UH.add env uri entity0; entity
+ELSE
+   let _, _, uri, _ = entity in
+   UH.add env uri entity; entity
+END
 
 let get_entity uri =
    try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void