]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgEnvironment.ml
- bug fix in the static analyzer allows better Pi/forall separation (exportation...
[helm.git] / helm / software / helena / src / basic_rg / brgEnvironment.ml
index 0fbbd9a543072748d7968d4fc034cb88cdccd703..1b3f744e2b43a3469ed04deb4814dba32b073a7c 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,9 @@ let env = UH.create hsize
 
 (* decps *)
 let set_entity entity =
-   let _, _, uri, _ = entity in
-   UH.add env uri entity; entity
+   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
 
 let get_entity uri =
    try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void