From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 27 Jun 2015 18:35:52 +0000 (+0000)
Subject: - bug fix in the static analyzer allows better Pi/forall separation (exportation... 
X-Git-Tag: make_still_working~716
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;p=helm.git

- bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite)
- new option -y allows to use infinity-abstraction in contexts
- ages removed from global references (the RTM computes them)
- new semantics of the -g option (w.i.p.) for a comparison with Coq
---

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index 7babc30d3..a07afc02e 100644
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -126,10 +126,10 @@ src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \
     src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \
     src/basic_rg/brg.cmx src/common/alpha.cmx src/basic_rg/brgOutput.cmi
 src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx
-src/basic_rg/brgEnvironment.cmo : src/common/entity.cmx \
-    src/basic_rg/brgEnvironment.cmi
-src/basic_rg/brgEnvironment.cmx : src/common/entity.cmx \
-    src/basic_rg/brgEnvironment.cmi
+src/basic_rg/brgEnvironment.cmo : src/common/options.cmx \
+    src/common/entity.cmx src/basic_rg/brgEnvironment.cmi
+src/basic_rg/brgEnvironment.cmx : src/common/options.cmx \
+    src/common/entity.cmx src/basic_rg/brgEnvironment.cmi
 src/basic_rg/brgSubstitution.cmi : src/basic_rg/brg.cmx
 src/basic_rg/brgSubstitution.cmo : src/common/options.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi
diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 8ae171cd0..991d490f0 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -11,7 +11,7 @@ KEEP = README
 CLEAN = etc/log.txt etc/profile.txt
 
 TAGS = test-si-fast test-si test2 test3 test6 \
-       profile-fast profile profile-coq \
+       profile-fast profile profile-coq profile-coq-byte \
        xml-si xml-si-v3 xml xml-v3 \
        export-coq export-matita \
        export-lp1 export-lp2 export-tj2 export-tj3 \
@@ -19,7 +19,11 @@ TAGS = test-si-fast test-si test2 test3 test6 \
 
 include Makefile.common
 
-COQC = coqc
+TIME = `which time` -p -a -o etc/log.txt
+
+NULL = >/dev/null 2>&1 
+
+COQTOP = coqtop
 
 MATITAC = ../../../../matita/matita/matitac.opt
 
@@ -51,32 +55,32 @@ test-si: $(MAIN).opt etc
 	$(H)./$(MAIN).opt -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt
 
 test2: $(MAIN).opt etc
-	@echo "  HELENA -T 2 -d -l $(INPUT)"
-	$(H)./$(MAIN).opt -l -u $(INPUT) -X -T 2 -d -l $(O) $(INPUT) > etc/log.txt
+	@echo "  HELENA -T 2 -l $(INPUT)"
+	$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l $(O) $(INPUT) > etc/log.txt
 
 test3: $(MAIN).opt etc
-	@echo "  HELENA -T 3 -d -l $(INPUT)"
-	$(H)./$(MAIN).opt -l -u $(INPUT) -X -T 3 -d -l $(O) $(INPUT) > etc/log.txt
+	@echo "  HELENA -T 3 -l $(INPUT)"
+	$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 3 -l $(O) $(INPUT) > etc/log.txt
 
 test6: $(MAIN).opt etc
-	@echo "  HELENA -T 6 -d -l -n $(INPUT)"
-	$(H)./$(MAIN).opt -l -u $(INPUT) -X -T 6 -d -l -n $(O) $(INPUT) > etc/log.txt
+	@echo "  HELENA -T 6 -l $(INPUT)"
+	$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt
 
 xml-si: $(MAIN).opt etc
 	@echo "  HELENA -l -o -s 1 -u $(INPUT)"
-	$(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(O) $(INPUT) > etc/log.txt
 
 xml-si-v3: $(MAIN).opt etc
 	@echo "  HELENA -l -o -s 2 -u $(INPUT)"
-	$(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(O) $(INPUT) > etc/log.txt
 
 xml: $(MAIN).opt etc
 	@echo "  HELENA -l -o -s 1 $(INPUT)"
-	$(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(O) $(INPUT) > etc/log.txt
 
 xml-v3: $(MAIN).opt etc
 	@echo "  HELENA -l -o -s 2 $(INPUT)"
-	$(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(O) $(INPUT) > etc/log.txt
 
 export-coq coq/$(V): $(MAIN).opt etc
 	@echo "  HELENA -l -m V8 -u $(INPUT)"
@@ -115,9 +119,15 @@ profile: $(MAIN).opt etc
 	$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
 
 profile-coq: $(MAIN).opt etc
-	@echo "  COQC $(V) (31 TIMES)"
+	@echo "  COQTOP $(V) (31 TIMES)"
+	$(H)rm -f etc/log.txt
+	$(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP) -q  $(NULL); done
+	$(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt
+
+profile-coq-byte: $(MAIN).opt etc
+	@echo "  COQTOP $(V) (31 TIMES)"
 	$(H)rm -f etc/log.txt
-	$(H)for _ in `seq 31`; do `which time` -p -a -u etc/log.txt $(COQC) coq/$(V); done
+	$(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP).byte -q  $(NULL); done
 	$(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt
 
 matita: matita/$(MA)
diff --git a/helm/software/helena/coq/grundlagen_2.v b/helm/software/helena/coq/grundlagen_2.v
index b04a3e5dc..0d4f57cec 100644
--- a/helm/software/helena/coq/grundlagen_2.v
+++ b/helm/software/helena/coq/grundlagen_2.v
@@ -9,7 +9,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* This file was generated by Helena 0.8.2 M (February 2015): do not edit *)
+(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****)
 
 (* constant 1 *)
 Definition l_imp := (fun (a:Prop) => (fun (b:Prop) => ((forall (x:a), b) : Prop))).
diff --git a/helm/software/helena/matita/grundlagen_2.ma b/helm/software/helena/matita/grundlagen_2.ma
index 773c8a9de..304439b02 100644
--- a/helm/software/helena/matita/grundlagen_2.ma
+++ b/helm/software/helena/matita/grundlagen_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* This file was generated by Helena 0.8.2 M (February 2015): do not edit *)
+(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****)
 
 include "basics/pts.ma".
 
@@ -584,13 +584,13 @@ definition l_orec3_th1 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3
 definition l_orec3_th2 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3i c a b (l_or3_th5 a b c (l_orec3e1 a b c o)) (l_ec3_th5 a b c (l_orec3e2 a b c o)) : l_orec3 c a b).
 
 (* constant 190 *)
-axiom l_e_is : Πsigma:Type[0].Πs:sigma.Πt:sigma.Prop.
+axiom l_e_is : ∀sigma:Type[0].∀s:sigma.∀t:sigma.Prop.
 
 (* constant 191 *)
-axiom l_e_refis : Πsigma:Type[0].Πs:sigma.l_e_is sigma s s.
+axiom l_e_refis : ∀sigma:Type[0].∀s:sigma.l_e_is sigma s s.
 
 (* constant 192 *)
-axiom l_e_isp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.Πt:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t.
+axiom l_e_isp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀t:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t.
 
 (* constant 193 *)
 definition l_e_symis ≝ λsigma:Type[0].λs:sigma.λt:sigma.λi:l_e_is sigma s t.(l_e_isp sigma (λx:sigma.l_e_is sigma x s) s t (l_e_refis sigma s) i : l_e_is sigma t s).
@@ -650,10 +650,10 @@ definition l_e_onee1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma
 definition l_e_onee2 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.(l_ande2 (l_e_amone sigma p) (l_some sigma p) o1 : l_some sigma p).
 
 (* constant 212 *)
-axiom l_e_ind : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.sigma.
+axiom l_e_ind : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_one sigma p.sigma.
 
 (* constant 213 *)
-axiom l_e_oneax : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1).
+axiom l_e_oneax : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1).
 
 (* constant 214 *)
 definition l_e_one_th1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.λs:sigma.λsp:p s.(l_e_amonee sigma p (l_e_onee1 sigma p o1) (l_e_ind sigma p o1) s (l_e_oneax sigma p o1) sp : l_e_is sigma (l_e_ind sigma p o1) s).
@@ -788,25 +788,25 @@ definition l_e_bij_th1 ≝ λsigma:Type[0].λtau:Type[0].λupsilon:Type[0].λf:
 definition l_e_fise ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.(l_e_isp (Πx:sigma.tau) (λy:Πx:sigma.tau.l_e_is tau (f s) (y s)) f g (l_e_refis tau (f s)) i : l_e_is tau (f s) (g s)).
 
 (* constant 258 *)
-axiom l_e_fisi : Πsigma:Type[0].Πtau:Type[0].Πf:Πx:sigma.tau.Πg:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g.
+axiom l_e_fisi : ∀sigma:Type[0].∀tau:Type[0].∀f:Πx:sigma.tau.∀g:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g.
 
 (* constant 259 *)
 definition l_e_fis_th1 ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.λt:sigma.λj:l_e_is sigma s t.(l_e_tris tau (f s) (f t) (g t) (l_e_isf sigma tau f s t j) (l_e_fise sigma tau f g i t) : l_e_is tau (f s) (g t)).
 
 (* constant 260 *)
-axiom l_e_ot : Πsigma:Type[0].∀p:∀x:sigma.Prop.Type[0].
+axiom l_e_ot : Πsigma:Type[0].Πp:∀x:sigma.Prop.Type[0].
 
 (* constant 261 *)
-axiom l_e_in : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma.
+axiom l_e_in : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma.
 
 (* constant 262 *)
-axiom l_e_inp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.p (l_e_in sigma p o1).
+axiom l_e_inp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_ot sigma p.p (l_e_in sigma p o1).
 
 (* constant 263 *)
-axiom l_e_otax1 : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x).
+axiom l_e_otax1 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x).
 
 (* constant 264 *)
-axiom l_e_otax2 : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s.
+axiom l_e_otax2 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s.
 
 (* constant 265 *)
 definition l_e_isini ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_ot sigma p.λo2:l_e_ot sigma p.λi:l_e_is (l_e_ot sigma p) o1 o2.(l_e_isf (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) o1 o2 i : l_e_is sigma (l_e_in sigma p o1) (l_e_in sigma p o2)).
@@ -842,19 +842,19 @@ axiom l_e_first : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.sigm
 axiom l_e_second : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.tau.
 
 (* constant 276 *)
-axiom l_e_pairis1 : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1.
+axiom l_e_pairis1 : ∀sigma:Type[0].∀tau:Type[0].∀p1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1.
 
 (* constant 277 *)
 definition l_e_pairis2 ≝ λsigma:Type[0].λtau:Type[0].λp1:l_e_pairtype sigma tau.(l_e_symis (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1 (l_e_pairis1 sigma tau p1) : l_e_is (l_e_pairtype sigma tau) p1 (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1))).
 
 (* constant 278 *)
-axiom l_e_firstis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s.
+axiom l_e_firstis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s.
 
 (* constant 279 *)
 definition l_e_firstis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s (l_e_firstis1 sigma tau s t) : l_e_is sigma s (l_e_first sigma tau (l_e_pair sigma tau s t))).
 
 (* constant 280 *)
-axiom l_e_secondis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t.
+axiom l_e_secondis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t.
 
 (* constant 281 *)
 definition l_e_secondis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t (l_e_secondis1 sigma tau s t) : l_e_is tau t (l_e_second sigma tau (l_e_pair sigma tau s t))).
@@ -1208,16 +1208,16 @@ definition l_r_itef ≝ λa:Prop.λksi:Type[0].λx:Πt:a.ksi.λy:Πt:l_not a.ksi
 axiom l_e_st_set : Πsigma:Type[0].Type[0].
 
 (* constant 398 *)
-axiom l_e_st_esti : Πsigma:Type[0].Πs:sigma.Πs0:l_e_st_set sigma.Prop.
+axiom l_e_st_esti : ∀sigma:Type[0].∀s:sigma.∀s0:l_e_st_set sigma.Prop.
 
 (* constant 399 *)
-axiom l_e_st_setof : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_st_set sigma.
+axiom l_e_st_setof : Πsigma:Type[0].Πp:∀x:sigma.Prop.l_e_st_set sigma.
 
 (* constant 400 *)
-axiom l_e_st_estii : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p).
+axiom l_e_st_estii : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p).
 
 (* constant 401 *)
-axiom l_e_st_estie : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s.
+axiom l_e_st_estie : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s.
 
 (* constant 402 *)
 definition l_e_st_empty ≝ λsigma:Type[0].λs0:l_e_st_set sigma.(l_none sigma (λx:sigma.l_e_st_esti sigma x s0) : Prop).
@@ -1286,7 +1286,7 @@ definition l_e_st_isset_th1 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_s
 definition l_e_st_isset_th2 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λi:l_e_is (l_e_st_set sigma) s0 t0.(λx:sigma.λy:l_e_st_esti sigma x t0.l_e_st_issete2 sigma s0 t0 i x y : l_e_st_incl sigma t0 s0).
 
 (* constant 424 *)
-axiom l_e_st_isseti : Πsigma:Type[0].Πs0:l_e_st_set sigma.Πt0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0.
+axiom l_e_st_isseti : ∀sigma:Type[0].∀s0:l_e_st_set sigma.∀t0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0.
 
 (* constant 425 *)
 definition l_e_st_isset_th3 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λs:sigma.λses0:l_e_st_esti sigma s s0.λn:l_not (l_e_st_esti sigma s t0).(l_imp_th3 (l_e_is (l_e_st_set sigma) s0 t0) (l_e_st_esti sigma s t0) n (λt:l_e_is (l_e_st_set sigma) s0 t0.l_e_st_issete1 sigma s0 t0 t s ses0) : l_not (l_e_is (l_e_st_set sigma) s0 t0)).
diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 667b18cc1..22b3e799c 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -44,10 +44,19 @@ let empty_cnt = D.empty_lenv
 let alpha id =
    if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id
 
-let add_abst cnt id aw w =
+let attrs_for_abst id aw =
    let id = if !G.alpha <> "" then alpha id else id in
-   let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in 
-   D.EBind (cnt, aw, D.Abst (false, N.two, w))
+   let main = E.succ aw.E.n_main in
+   E.node_attrs ~name:(id, true) ~side:aw.E.n_main ~main ()
+
+let attrs_for_decl aw =
+   let main = E.succ aw.E.n_main in
+   E.node_attrs ~side:aw.E.n_main ~main ()
+
+let add_abst cnt id aw w =
+   let a = attrs_for_abst id aw in
+   let l = if !G.infinity then N.infinity else N.two in
+   D.EBind (cnt, a, D.Abst (false, l, w))
 
 let mk_lref f a i = f a (D.TLRef (a, i))
 
@@ -103,58 +112,66 @@ let get_cnt_relaxed f lst =
    get_cnt err f lst lst.node
 
 let push_abst f a w lenv =
-   let bw = D.Abst (false, N.infinite, w) in
+   let bw = D.Abst (false, N.infinity, w) in
    D.push_bind f a bw lenv
 
-let add_proj e t = match e with
+let add_proj at e t = match e with
    | D.ESort                 -> t
-   | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) 
-   | _                       -> D.TProj (E.empty_node, e, t)
+   | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) 
+   | _                       ->
+      let e = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start at e else e in
+      D.TProj (at, e, t)
 
 (* this is not tail recursive in the GRef branch *)
 let rec xlate_term f st lst y lenv = function
    | A.Sort s            ->
       let h = if s then 0 else 1 in
-      let a = E.node_attrs ~sort:h () in
+      let a = E.node_attrs ~main:(h, 0) () in
       f a (D.TSort (a, h))
    | A.Appl (v, t)       ->
-      let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in
-      let f _ vv = xlate_term (f vv) st lst y lenv t in
+      let f av vv at tt =
+         let at = E.compose av at in
+         f at (D.TAppl (at, !G.extended, vv, tt))
+      in
+      let f av vv = xlate_term (f av vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
-      let name = if !G.alpha <> "" then alpha name else name in
-      let name = Some (name, true) in
-      let f aw ww = 
+      let f aw ww =
+         let aw = attrs_for_abst name aw in
          let f at tt =
+	    let at = E.compose aw at in
             let l = 
-               if !G.cc then match y, at.E.n_degr with
+               if !G.cc then match y, snd at.E.n_main with
                   | true, _ -> N.one
                   | _   , 0 -> N.one
                   | _   , 1 -> N.unknown st
                   | _   , 2 -> N.two
                   | _       -> assert false
-               else N.infinite
+               else N.infinity
             in
 	    let b = D.Abst (false, l, ww) in
-	    let at = {at with E.n_name = name} in
 	    f at (D.TBind (at, b, tt))
 	 in
          let f lenv = xlate_term f st lst y lenv t in
-	 push_abst f {aw with E.n_name = name; E.n_degr = succ aw.E.n_degr} ww lenv
+	 push_abst f aw ww lenv
       in
       xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
       let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
       let map2 f arg args = 
-         let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in 
+         let f av v = f (D.EAppl (args, E.shift av, !G.extended, v)) in 
          xlate_term f st lst false lenv arg
       in
       let g qid a cnt =
          let gref = D.TGRef (a, uri_of_qid qid) in
 	 if cnt = D.ESort then f a gref else
 	 let f = function 
-            | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref))
-            | args                       -> f a (D.TProj (a, args, gref))
+            | D.EAppl (D.ESort, av, x, v) ->
+               let a = E.compose av a in
+               f a (D.TAppl (a, x, v, gref))
+            | args                        ->
+               let args = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start a args else args in
+               f a (D.TProj (a, args, gref))
          in
 	 let f args = C.list_fold_right f map2 args D.ESort in
 	 D.sub_list_strict (D.fold_names f map1 args) cnt args
@@ -193,14 +210,14 @@ let xlate_entity err f st lst = function
       let f lenv =
 	 let f qid = 
             let f aw ww =
-               let aw = {aw with E.n_apix = lst.line; E.n_degr = succ aw.E.n_degr} in
-               UH.add henv (uri_of_qid qid) (aw, lenv);
-	       let t = add_proj lenv ww in
+               let a = attrs_for_decl aw in
+               UH.add henv (uri_of_qid qid) (a, lenv);
+	       let t = add_proj aw lenv ww in
 (*
 	    print_newline (); CrgOutput.pp_term print_string t;
 *)
-	       let b = E.Abst t in
-	       let entity = E.empty_root, aw, uri_of_qid qid, b in
+               let na = {aw with E.n_apix = lst.line} in
+	       let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
                G.set_current_trace lst.line;
 	       f {lst with line = succ lst.line} entity
 	    in
@@ -208,21 +225,21 @@ let xlate_entity err f st lst = function
 	 in
          complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed (D.replace f N.one) lst
+      let f = if !G.infinity then f else D.set_layer f N.one in 
+      get_cnt_relaxed f lst
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
             let f _ ww =
 	       let f av vv =
-                  let na = {av with E.n_apix = lst.line} in
-                  UH.add henv (uri_of_qid qid) (na, lenv);
-                  let t = add_proj lenv (D.TCast (na, ww, vv)) in
+                  UH.add henv (uri_of_qid qid) (av, lenv);
+                  let t = add_proj av lenv (D.TCast (av, ww, vv)) in
 (*
 	    print_newline (); CrgOutput.pp_term print_string t;
 *)
-	          let b = E.Abbr t in
+                  let na = {av with E.n_apix = lst.line} in
                   let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
-	          let entity = ra, na, uri_of_qid qid, b in
+	          let entity = ra, na, uri_of_qid qid, E.Abbr t in
                   G.set_current_trace lst.line;
 	          f {lst with line = succ lst.line} entity
 	       in
diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
index b9ce1d344..cb21d0247 100644
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -78,7 +78,7 @@ let rec xlate_bk_term f c = function
 
 and xlate_bk_bind f c = function
    | Z.Abst t ->
-      let f tt = f (D.Abst (false, N.infinite, tt)) in
+      let f tt = f (D.Abst (false, N.infinity, tt)) in
       xlate_bk_term f c t
    | Z.Abbr t ->
       let f tt = f (D.Abbr tt) in
diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml
index a321a32b0..a39010f80 100644
--- a/helm/software/helena/src/basic_rg/brg.ml
+++ b/helm/software/helena/src/basic_rg/brg.ml
@@ -46,6 +46,8 @@ let abbr v = Abbr v
 
 let lref a i = LRef (a, i)
 
+let gref a u = GRef (a, u)
+
 let cast a u t = Cast (a, u, t)
 
 let appl a x u t = Appl (a, x, u, t)
diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml
index 0fbbd9a54..1b3f744e2 100644
--- a/helm/software/helena/src/basic_rg/brgEnvironment.ml
+++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml
@@ -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
diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml
index caa8ab465..bdb78144a 100644
--- a/helm/software/helena/src/basic_rg/brgGallina.ml
+++ b/helm/software/helena/src/basic_rg/brgGallina.ml
@@ -111,13 +111,14 @@ let rec out_term st p e och = function
 
 let close_out och () = close_out och
 
-let output_entity och st (_, na, s, b) =
+let output_entity och st (_, na, u, b) =
    out_comment och (KP.sprintf "constant %u" na.E.n_apix);
    match b with
-      | E.Abbr t ->
-         KP.fprintf och "Definition %a := %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
-      | E.Abst t ->
-         KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+      | E.Abbr v ->
+         KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
+(*         KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
+      | E.Abst w ->
+         KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok
       | E.Void   -> C.err ()
 
 (* Interface functions ******************************************************)
@@ -128,5 +129,4 @@ let open_out fname =
    let och = open_out (path ^ ext) in
    out_preamble och;
    out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
-(*   out_include och "basics/pts"; *)
    output_entity och, close_out och
diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index 71b189dac..b1cfe21ca 100644
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -88,7 +88,7 @@ let rec out_term st p e och = function
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
       let ee = B.push e B.empty a (B.abst r n w) in
-      let binder = match N.to_string st n, a.E.n_sort with
+      let binder = match N.to_string st n, fst a.E.n_main with
          | "1", 0 -> "Π"
          | "1", 1 -> "∀"
          | "2", _ -> "λ"
@@ -106,13 +106,13 @@ let rec out_term st p e och = function
 
 let close_out och () = close_out och
 
-let output_entity och st (_, na, s, b) =
+let output_entity och st (_, na, u, b) =
    out_comment och (KP.sprintf "constant %u" na.E.n_apix);
    match b with
-      | E.Abbr t ->
-         KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
-      | E.Abst t ->
-         KP.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+      | E.Abbr v ->
+         KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok
+      | E.Abst w ->
+         KP.fprintf och "axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok
       | E.Void   -> C.err ()
 
 (* Interface functions ******************************************************)
diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 1a5a3f1cf..f20335193 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -101,12 +101,8 @@ let rec step st m r =
       else m, r, None
    | B.GRef (_, uri)                     ->
       begin match BE.get_entity uri with
-         | _, _, _, E.Abbr v ->
-            if !G.expand then begin
-	       if !G.summary then O.add ~gdelta:1 ();
-               step st m v
-            end else
-	       m, r, Some v
+         | _, a, _, E.Abbr v ->
+	       m, B.gref a uri, Some v
          | _, _, _, E.Abst w ->
             if assert_tstep m true then begin
                if !G.summary then O.add ~grt:1 (); 
@@ -126,7 +122,7 @@ let rec step st m r =
                if !G.summary then O.add ~lrt:1 ();
                step st {(tstep m) with e = c} w
             end else
-	       m, B.LRef (a, i), None
+	       m, B.lref a i, None
 	 | _, _, B.Void           ->
 	    assert false
       end
diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml
index c53db162b..d834ed53e 100644
--- a/helm/software/helena/src/common/entity.ml
+++ b/helm/software/helena/src/common/entity.ml
@@ -18,6 +18,8 @@ type id = string (* identifier *)
 
 type name = id * bool (* token, real? *)
 
+type arity = int * int (* sort, degree *)
+
 type meta = Main     (* main object *)
           | InProp   (* inhabitant of a proposition *)
           | Progress (* uncompleted object *)
@@ -26,8 +28,8 @@ type meta = Main     (* main object *)
 type node_attrs = {
    n_name: name option; (* name *)
    n_apix: int;         (* additional position index *)
-   n_degr: int;         (* degree *)
-   n_sort: int;         (* sort *)
+   n_main: arity;       (* main arity *)
+   n_side: arity;       (* side arity *)
 }
 
 type root_attrs = {
@@ -43,8 +45,8 @@ type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, bi
 
 (* helpers ******************************************************************)
 
-let node_attrs ?(apix=0) ?name ?(degr=0) ?(sort=0) () = {
-   n_apix = apix; n_name = name; n_degr = degr; n_sort = sort
+let node_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = {
+   n_apix = 0; n_name = name; n_main = main; n_side = side;
 }
 
 let root_attrs ?(meta=[]) ?info () = {
@@ -57,6 +59,12 @@ let empty_root = root_attrs ()
 
 let common f (ra, na, u, _) = f ra na u
 
+let succ (sort, degr) = sort, succ degr
+
+let compose av at = {av with n_main = at.n_main}
+
+let shift av = {av with n_side = av.n_main}
+
 let rec name err f a = match a.n_name with
    | Some (n, r) -> f n r
    | None        -> err ()
diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index 1ad6cf28c..de8b98254 100644
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -123,7 +123,7 @@ let initial_status () =
 
 let refresh_status st = st 
 
-let infinite = cell true Inf
+let infinity = cell true Inf
 
 let finite i = cell true (Fin i)
 
diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli
index 40ada03a1..f6abb1195 100644
--- a/helm/software/helena/src/common/layer.mli
+++ b/helm/software/helena/src/common/layer.mli
@@ -17,7 +17,7 @@ val initial_status: unit -> status
 
 val refresh_status: status -> status
 
-val infinite: layer
+val infinity: layer
 
 val finite: int -> layer
 
diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 3ac27296d..b2dc97292 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -27,7 +27,7 @@ type manager = Quiet
 
 (* interface functions ******************************************************)
 
-let version_string = "Helena 0.8.2 M (June 2015)"
+let version_string = "Helena 0.8.3 M (June 2015)"
 
 let stage = ref 3            (* stage *)
 
@@ -37,6 +37,8 @@ let ct = ref 0               (* current trace level *)
 
 let summary = ref false      (* log summary information *)
 
+let export = ref false       (* export entities to XML *)
+
 let xdir = ref ""            (* directory for XML output *)
 
 let kernel = ref V3          (* kernel type *)
@@ -73,6 +75,8 @@ let last = ref max_int       (* end trace here *)
 
 let extended = ref false     (* extended applications *) 
 
+let infinity = ref false     (* use ∞-abstractions in contexts *) 
+
 let short = ref false        (* short global constants *) 
 
 let set_current_trace n =
@@ -96,8 +100,8 @@ let get_mk_uri () =
    fun s -> KF.concat bu (s ^ ".ld")
 
 let clear () =
-   stage := 3; trace := 0; summary := false; first := 0; last := max_int;
-   xdir := ""; kernel := V3; si := false; extended := false; cover := ""; 
+   stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int;
+   xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false; short := false;
    debug_parser := false; debug_lexer := false;
    manager_dir := ""; manager := Quiet
diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml
index 94bf217da..3c813b275 100644
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -43,6 +43,7 @@ let add
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
 =
+(*
    if !G.ct >= level then begin
       if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
       if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
@@ -50,6 +51,7 @@ let add
       if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
       if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
    end;
+*)
 reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index ea3ec54bf..a250d3edd 100644
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -115,13 +115,28 @@ let rec mem err f e b = match e with
    | EProj (e, _, d)    -> 
       let err () = mem err f e b in mem err f d b
 
-let replace f n0 e =
+let set_layer f n0 e =
    let rec aux f = function
       | ESort                        -> f ESort
       | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
       | EBind (e, a, b)              -> aux (push_bind f a b) e
       | EAppl (e, a, x, v)           -> aux (push_appl f a x v) e
       | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
+   in
+   aux f e
 
+let set_attrs f a0 e =
+   let rec aux f = function
+      | ESort              -> f ESort
+      | EBind (e, a, b)    -> 
+         let a = E.compose a a0 in
+         aux (push_bind f a b) e
+      | EAppl (e, a, x, v) ->
+         let a = E.compose a a0 in
+         aux (push_appl f a x v) e
+      | EProj (e, a, d)    ->
+         let a = E.compose a a0 in
+         let f d = aux (push_proj f a d) e in
+         aux f d
    in
    aux f e
diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index b2d0c99e1..1ba830669 100644
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -66,7 +66,7 @@ let rec xlate_term f st lenv = function
    Printf.printf "\n";
 *)
    | T.Sort h         ->
-      let a = E.node_attrs ~sort:h () in 
+      let a = E.node_attrs ~main:(h, 0) () in 
       f a (D.TSort (a, h))
    | T.NSrt id        ->
       let f h = xlate_term f st lenv (T.Sort h) in
@@ -115,7 +115,7 @@ and xlate_bind st f (lenv, e) b =
          in
          xlate_term f st lenv v
       | T.Void id           ->
-         let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
+         let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
          f a D.Void
 
 let mk_contents main kind tt =
diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly
index d08fb87d9..32d0df309 100644
--- a/helm/software/helena/src/text/txtParser.mly
+++ b/helm/software/helena/src/text/txtParser.mly
@@ -68,7 +68,7 @@
       | sort CM sorts { $1 :: $3 }
    ;
    layer:
-      |       { N.infinite  }
+      |       { N.infinity  }
       | CT IX { N.finite $2 }
    ;
 
diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 0f953949e..3e7f8aa91 100644
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -219,7 +219,6 @@ let count_input st = function
 let version = ref true
 let preprocess = ref false
 let root = ref ""
-let export = ref false
 let st = ref (initial_status ())
 let streaming = ref false (* parsing style (temporary) *)
 
@@ -230,7 +229,7 @@ let process_2 st entity =
          let f = if !version then validate else type_check in f st entity
       else st
    in
-   if !export then export_entity st entity;
+   if !G.export then export_entity st entity;
    match st.mst with
      | None                    -> st
      | Some (export_entity, _) -> manager st export_entity entity
@@ -238,7 +237,7 @@ let process_2 st entity =
 let process_1 st entity = 
    if !G.ct >= 3 then pp_progress entity;
    let st = if !G.summary then count_entity st entity else st in
-   if !export && !G.stage = 1 then export_entity st entity;
+   if !G.export && !G.stage = 1 then export_entity st entity;
    if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st 
 
 let process_0 st entity = 
@@ -322,7 +321,7 @@ let main =
       | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
    in
    let clear_options () =
-      export := false; preprocess := false;
+      preprocess := false;
       root := "";
       G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
@@ -363,7 +362,7 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilnoqtux01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
@@ -396,7 +395,8 @@ let main =
    let help_s = "<number> [stage]     Set translation stage (see above)" in
    let help_t = "         [type]      Type check (default: validate)" in
    let help_u = "         [upsilon]   Activate type comparison by sort inclusion (default: false)" in
-   let help_x = "         [extended]  Use extended applications (Automath)" in   
+   let help_x = "         [extended]  Use extended applications (Automath)" in
+   let help_y = "         [infinity]  Use ∞-abstractions in contexts" in
    let help_0 = "         [zero]      Preprocess source (Automath)" in
    let help_1 = "         [one]       parse files with streaming policy" in
    at_exit exit;
@@ -419,7 +419,7 @@ let main =
       ("-l", Arg.Set G.cc, help_l);
       ("-m", Arg.String set_manager, help_m);      
       ("-n", Arg.Set G.short, help_n);
-      ("-o", Arg.Set export, help_o);
+      ("-o", Arg.Set G.export, help_o);
       ("-p", Arg.String ((:=) G.preamble), help_p);
       ("-q", Arg.Set G.unquote, help_q);      
       ("-r", Arg.String ((:=) root), help_r);
@@ -427,6 +427,7 @@ let main =
       ("-t", Arg.Clear version, help_t);      
       ("-u", Arg.Set G.si, help_u);
       ("-x", Arg.Set G.extended, help_x);
+      ("-y", Arg.Set G.infinity, help_y);
       ("-0", Arg.Unit set_preprocess, help_0);
       ("-1", Arg.Set streaming, help_1);      
    ] process_file help
diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index b5e3b9b40..b04f5f6e1 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -22,7 +22,7 @@ module D  = Crg
 let lenv_iter map_bind map_appl map_proj st e lenv out tab = 
    let rec aux = function
       | D.ESort           -> e
-      | D.EBind (e, a, b) -> 
+      | D.EBind (e, a, b) ->
          let e = aux e in
 (* NOTE: the inner binders are alpha-converted first *)
          let a = R.alpha D.mem e a in
@@ -51,11 +51,11 @@ let rec exp_term st e t out tab = match t with
 	 let f n r = {a with E.n_name = Some (n, r)} in
          D.get_name err f i e
       in
-      let attrs = [XL.position i; XL.name a] in
+      let attrs = [XL.position i; XL.name a ] in
       XL.tag XL.lref attrs out tab
    | D.TGRef (a, n)       ->
       let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
-      let attrs = [XL.uri n; XL.name a; XL.apix a] in
+      let attrs = [XL.uri n; XL.name a ] in
       XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
       let attrs = [] in
@@ -81,7 +81,7 @@ and exp_appl st e a x v out tab =
 
 and exp_bind st e a b out tab = match b with
    | D.Abst (_, n, w) ->
-      let attrs = [XL.layer st n; XL.name a; XL.kind a] in
+      let attrs = XL.layer st n :: XL.name a :: XL.main a in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v         ->
       let attrs = [XL.name a] in
diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 3c77fe68b..dcc18c94b 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -96,14 +96,23 @@ let name a =
    let f n r = "name", if r then n else "-" ^ n in 
    E.name err f a
 
-let apix a =
-   "position", string_of_int a.E.n_apix
-
 let layer st n =
    "layer", N.to_string st n
 
-let kind a =
-   "position", string_of_int a.E.n_sort
+let main a =
+   let sort, degr = a.E.n_main in
+   ["main-sort", string_of_int sort;
+    "main-degree", string_of_int degr;
+   ]
+
+let side a =
+   let sort, degr = a.E.n_side in
+   ["side-sort", string_of_int sort;
+    "side-degree", string_of_int degr;
+   ]
+
+let apix a =
+   "level", string_of_int a.E.n_apix
 
 let meta a =
    let map = function
diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli
index 4ac5dc913..e49d0e8d8 100644
--- a/helm/software/helena/src/xml/xmlLibrary.mli
+++ b/helm/software/helena/src/xml/xmlLibrary.mli
@@ -45,9 +45,11 @@ val layer: Layer.status -> Layer.layer -> attr
 
 val name: Entity.node_attrs -> attr
 
-val apix: Entity.node_attrs -> attr
+val main: Entity.node_attrs -> attr list
+
+val side: Entity.node_attrs -> attr list
 
-val kind: Entity.node_attrs -> attr
+val apix: Entity.node_attrs -> attr
 
 val meta: Entity.root_attrs -> attr