]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgEnvironment.ml
we are optimizing the code by conditional compilation.
[helm.git] / helm / software / helena / src / basic_rg / brgEnvironment.ml
index 1b3f744e2b43a3469ed04deb4814dba32b073a7c..231027ad8799217e7a47b69e5ac18b924bb5dd8b 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
    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