]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgEnvironment.ml
helena: warning removed and modifications for λΥP exportation
[helm.git] / helm / software / helena / src / basic_rg / brgEnvironment.ml
index 0fbbd9a543072748d7968d4fc034cb88cdccd703..01a38f89ffeffa52e296b023b3816d083f0389f0 100644 (file)
@@ -11,6 +11,7 @@
 
 module U  = NUri
 module UH = U.UriHash
+module G  = Options
 module E  = Entity
 
 let hsize = 7000 
@@ -20,8 +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, 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