- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / common / entity.ml

diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml
index c447190501854daee08e11455956be0ae1477105..f616b780c54bf368f74f8be7d5d80f870d9b0f28 100644 (file)
--- a/helm/software/helena/src/common/entity.ml
+++ b/helm/software/helena/src/common/entity.ml
@@ -27,7 +27,6 @@ type node_attrs = {
    n_name: name option; (* name *)
    n_apix: int option;  (* additional position index *)
    n_degr: int;         (* degree *)
-   n_real: bool;        (* real node? (not generated) *)
 }
 
 type root_attrs = {
@@ -39,12 +38,12 @@ type 'term bind = Abst of 'term (* declaration: domain *)
                 | Abbr of 'term (* definition: body    *)
                | Void          (* exclusion           *)
 
-type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs,  uri, binder *)
+type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, binder *)
 
 (* helpers ******************************************************************)
 
 let node_attrs ?(real=true) ?apix ?name ?(degr=0) () = {
-   n_real = real; n_apix = apix; n_name = name; n_degr = degr;
+   n_apix = apix; n_name = name; n_degr = degr;
 }
 
 let root_attrs ?(meta=[]) ?info () = {