From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 14 Dec 2014 19:17:51 +0000 (+0000)
Subject: - we are moving from old (patched) management of sort inclusion
X-Git-Tag: make_still_working~783
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;p=helm.git

- we are moving from old (patched) management of sort inclusion
  to new (proper) one via \lambda\delta 3
- some refactoring
- omega.out: committed for reference
- Makefiles: some bugs fixed
---

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index 0580e6bfc..b6d1f4d83 100644
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -15,13 +15,13 @@ src/common/marks.cmx : src/common/marks.cmi
 src/common/hierarchy.cmi :
 src/common/hierarchy.cmo : src/lib/cps.cmx src/common/hierarchy.cmi
 src/common/hierarchy.cmx : src/lib/cps.cmx src/common/hierarchy.cmi
-src/common/level.cmi :
-src/common/level.cmo : src/common/options.cmx src/common/marks.cmi \
-    src/lib/log.cmi src/common/level.cmi
-src/common/level.cmx : src/common/options.cmx src/common/marks.cmx \
-    src/lib/log.cmx src/common/level.cmi
-src/common/entity.cmo : src/common/level.cmi
-src/common/entity.cmx : src/common/level.cmx
+src/common/layer.cmi :
+src/common/layer.cmo : src/common/options.cmx src/common/marks.cmi \
+    src/lib/log.cmi src/common/layer.cmi
+src/common/layer.cmx : src/common/options.cmx src/common/marks.cmx \
+    src/lib/log.cmx src/common/layer.cmi
+src/common/entity.cmo : src/common/layer.cmi
+src/common/entity.cmx : src/common/layer.cmx
 src/common/output.cmi :
 src/common/output.cmo : src/common/options.cmx src/lib/log.cmi \
     src/common/output.cmi
@@ -30,26 +30,24 @@ src/common/output.cmx : src/common/options.cmx src/lib/log.cmx \
 src/common/alpha.cmi : src/common/entity.cmx
 src/common/alpha.cmo : src/common/entity.cmx src/common/alpha.cmi
 src/common/alpha.cmx : src/common/entity.cmx src/common/alpha.cmi
-src/common/status.cmo : src/common/options.cmx src/common/level.cmi
-src/common/status.cmx : src/common/options.cmx src/common/level.cmx
-src/complete_rg/crg.cmo : src/common/level.cmi src/common/entity.cmx \
+src/complete_rg/crg.cmo : src/common/layer.cmi src/common/entity.cmx \
     src/lib/cps.cmx
-src/complete_rg/crg.cmx : src/common/level.cmx src/common/entity.cmx \
+src/complete_rg/crg.cmx : src/common/layer.cmx src/common/entity.cmx \
     src/lib/cps.cmx
-src/complete_rg/crgOutput.cmi : src/common/level.cmi src/complete_rg/crg.cmx
+src/complete_rg/crgOutput.cmi : src/common/layer.cmi src/complete_rg/crg.cmx
 src/complete_rg/crgOutput.cmo : src/common/marks.cmi src/lib/log.cmi \
-    src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+    src/common/layer.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
     src/lib/cps.cmx src/complete_rg/crgOutput.cmi
 src/complete_rg/crgOutput.cmx : src/common/marks.cmx src/lib/log.cmx \
-    src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+    src/common/layer.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
     src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/text/txt.cmo : src/common/level.cmi
-src/text/txt.cmx : src/common/level.cmx
+src/text/txt.cmo : src/common/layer.cmi
+src/text/txt.cmx : src/common/layer.cmx
 src/text/txtParser.cmi : src/text/txt.cmx
 src/text/txtParser.cmo : src/text/txt.cmx src/common/options.cmx \
-    src/common/level.cmi src/text/txtParser.cmi
+    src/common/layer.cmi src/text/txtParser.cmi
 src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \
-    src/common/level.cmx src/text/txtParser.cmi
+    src/common/layer.cmx src/text/txtParser.cmi
 src/text/txtLexer.cmo : src/text/txtParser.cmi src/common/options.cmx \
     src/lib/log.cmi
 src/text/txtLexer.cmx : src/text/txtParser.cmx src/common/options.cmx \
@@ -88,22 +86,22 @@ src/automath/autLexer.cmo : src/common/options.cmx src/lib/log.cmi \
     src/automath/autParser.cmi
 src/automath/autLexer.cmx : src/common/options.cmx src/lib/log.cmx \
     src/automath/autParser.cmx
-src/automath/autCrg.cmi : src/common/status.cmx src/complete_rg/crg.cmx \
+src/automath/autCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \
     src/automath/aut.cmx
-src/automath/autCrg.cmo : src/common/status.cmx src/common/options.cmx \
-    src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
-    src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi
-src/automath/autCrg.cmx : src/common/status.cmx src/common/options.cmx \
-    src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
-    src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi
-src/xml/xmlLibrary.cmi : src/common/level.cmi src/common/entity.cmx
-src/xml/xmlLibrary.cmo : src/common/options.cmx src/common/level.cmi \
+src/automath/autCrg.cmo : src/common/options.cmx src/common/layer.cmi \
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/automath/aut.cmx src/automath/autCrg.cmi
+src/automath/autCrg.cmx : src/common/options.cmx src/common/layer.cmx \
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/automath/aut.cmx src/automath/autCrg.cmi
+src/xml/xmlLibrary.cmi : src/common/layer.cmi src/common/entity.cmx
+src/xml/xmlLibrary.cmo : src/common/options.cmx src/common/layer.cmi \
     src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
     src/xml/xmlLibrary.cmi
-src/xml/xmlLibrary.cmx : src/common/options.cmx src/common/level.cmx \
+src/xml/xmlLibrary.cmx : src/common/options.cmx src/common/layer.cmx \
     src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
     src/xml/xmlLibrary.cmi
-src/xml/xmlCrg.cmi : src/xml/xmlLibrary.cmi src/common/level.cmi \
+src/xml/xmlCrg.cmi : src/xml/xmlLibrary.cmi src/common/layer.cmi \
     src/complete_rg/crg.cmx
 src/xml/xmlCrg.cmo : src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
     src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
@@ -111,23 +109,23 @@ src/xml/xmlCrg.cmo : src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
 src/xml/xmlCrg.cmx : src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \
     src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
     src/common/alpha.cmx src/xml/xmlCrg.cmi
-src/basic_rg/brg.cmo : src/common/level.cmi src/common/entity.cmx
-src/basic_rg/brg.cmx : src/common/level.cmx src/common/entity.cmx
+src/basic_rg/brg.cmo : src/common/layer.cmi src/common/entity.cmx
+src/basic_rg/brg.cmx : src/common/layer.cmx src/common/entity.cmx
 src/basic_rg/brgCrg.cmi : src/complete_rg/crg.cmx src/basic_rg/brg.cmx
-src/basic_rg/brgCrg.cmo : src/common/level.cmi src/common/entity.cmx \
+src/basic_rg/brgCrg.cmo : src/common/layer.cmi src/common/entity.cmx \
     src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgCrg.cmi
-src/basic_rg/brgCrg.cmx : src/common/level.cmx src/common/entity.cmx \
+src/basic_rg/brgCrg.cmx : src/common/layer.cmx src/common/entity.cmx \
     src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgCrg.cmi
 src/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \
-    src/common/level.cmi src/basic_rg/brg.cmx
+    src/common/layer.cmi src/basic_rg/brg.cmx
 src/basic_rg/brgOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \
-    src/lib/log.cmi src/common/level.cmi src/common/hierarchy.cmi \
+    src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \
     src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmi \
     src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
 src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \
-    src/lib/log.cmx src/common/level.cmx src/common/hierarchy.cmx \
+    src/lib/log.cmx src/common/layer.cmx src/common/hierarchy.cmx \
     src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
 src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx
@@ -140,43 +138,41 @@ src/basic_rg/brgSubstitution.cmo : src/common/options.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi
 src/basic_rg/brgSubstitution.cmx : src/common/options.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi
-src/basic_rg/brgReduction.cmi : src/common/status.cmx src/lib/log.cmi \
-    src/common/level.cmi src/common/entity.cmx src/basic_rg/brg.cmx
-src/basic_rg/brgReduction.cmo : src/common/status.cmx src/lib/share.cmx \
-    src/common/output.cmi src/common/options.cmx src/lib/log.cmi \
-    src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \
-    src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \
-    src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi
-src/basic_rg/brgReduction.cmx : src/common/status.cmx src/lib/share.cmx \
-    src/common/output.cmx src/common/options.cmx src/lib/log.cmx \
-    src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \
-    src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \
-    src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi
-src/basic_rg/brgValidity.cmi : src/common/status.cmx \
+src/basic_rg/brgReduction.cmi : src/lib/log.cmi src/common/layer.cmi \
+    src/common/entity.cmx src/basic_rg/brg.cmx
+src/basic_rg/brgReduction.cmo : src/lib/share.cmx src/common/output.cmi \
+    src/common/options.cmx src/lib/log.cmi src/common/layer.cmi \
+    src/common/hierarchy.cmi src/common/entity.cmx src/basic_rg/brgOutput.cmi \
+    src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
+    src/basic_rg/brgReduction.cmi
+src/basic_rg/brgReduction.cmx : src/lib/share.cmx src/common/output.cmx \
+    src/common/options.cmx src/lib/log.cmx src/common/layer.cmx \
+    src/common/hierarchy.cmx src/common/entity.cmx src/basic_rg/brgOutput.cmx \
+    src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
+    src/basic_rg/brgReduction.cmi
+src/basic_rg/brgValidity.cmi : src/common/layer.cmi \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
-src/basic_rg/brgValidity.cmo : src/common/status.cmx src/common/options.cmx \
-    src/lib/log.cmi src/common/entity.cmx src/basic_rg/brgReduction.cmi \
+src/basic_rg/brgValidity.cmo : src/common/options.cmx src/lib/log.cmi \
+    src/common/entity.cmx src/basic_rg/brgReduction.cmi \
     src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
     src/basic_rg/brgValidity.cmi
-src/basic_rg/brgValidity.cmx : src/common/status.cmx src/common/options.cmx \
-    src/lib/log.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \
+src/basic_rg/brgValidity.cmx : src/common/options.cmx src/lib/log.cmx \
+    src/common/entity.cmx src/basic_rg/brgReduction.cmx \
     src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgValidity.cmi
-src/basic_rg/brgType.cmi : src/common/status.cmx \
+src/basic_rg/brgType.cmi : src/common/layer.cmi \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
-src/basic_rg/brgType.cmo : src/common/status.cmx src/lib/share.cmx \
-    src/common/options.cmx src/lib/log.cmi src/common/level.cmi \
-    src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
-    src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \
-    src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
-    src/basic_rg/brgType.cmi
-src/basic_rg/brgType.cmx : src/common/status.cmx src/lib/share.cmx \
-    src/common/options.cmx src/lib/log.cmx src/common/level.cmx \
-    src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
-    src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \
-    src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
-    src/basic_rg/brgType.cmi
-src/basic_rg/brgUntrusted.cmi : src/common/status.cmx \
+src/basic_rg/brgType.cmo : src/lib/share.cmx src/common/options.cmx \
+    src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \
+    src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgSubstitution.cmi \
+    src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \
+    src/basic_rg/brg.cmx src/basic_rg/brgType.cmi
+src/basic_rg/brgType.cmx : src/lib/share.cmx src/common/options.cmx \
+    src/lib/log.cmx src/common/layer.cmx src/common/hierarchy.cmx \
+    src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \
+    src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
+    src/basic_rg/brg.cmx src/basic_rg/brgType.cmi
+src/basic_rg/brgUntrusted.cmi : src/common/layer.cmi \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
 src/basic_rg/brgUntrusted.cmo : src/lib/log.cmi src/common/entity.cmx \
     src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi \
@@ -186,27 +182,27 @@ src/basic_rg/brgUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \
     src/basic_rg/brgValidity.cmx src/basic_rg/brgType.cmx \
     src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
-src/basic_rg/brgGrafite.cmi : src/common/level.cmi src/basic_rg/brg.cmx
-src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/level.cmi \
+src/basic_rg/brgGrafite.cmi : src/common/layer.cmi src/basic_rg/brg.cmx
+src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/layer.cmi \
     src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
     src/common/alpha.cmi src/basic_rg/brgGrafite.cmi
-src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/level.cmx \
+src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/layer.cmx \
     src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
     src/common/alpha.cmx src/basic_rg/brgGrafite.cmi
 src/basic_ag/bag.cmo : src/common/marks.cmi src/lib/log.cmi \
     src/common/entity.cmx src/lib/cps.cmx
 src/basic_ag/bag.cmx : src/common/marks.cmx src/lib/log.cmx \
     src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bagCrg.cmi : src/common/level.cmi src/complete_rg/crg.cmx \
+src/basic_ag/bagCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \
     src/basic_ag/bag.cmx
-src/basic_ag/bagCrg.cmo : src/common/marks.cmi src/common/level.cmi \
+src/basic_ag/bagCrg.cmo : src/common/marks.cmi src/common/layer.cmi \
     src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
-src/basic_ag/bagCrg.cmx : src/common/marks.cmx src/common/level.cmx \
+src/basic_ag/bagCrg.cmx : src/common/marks.cmx src/common/layer.cmx \
     src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
 src/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \
-    src/common/level.cmi src/basic_ag/bag.cmx
+    src/common/layer.cmi src/basic_ag/bag.cmx
 src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \
     src/common/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \
     src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \
@@ -225,29 +221,29 @@ src/basic_ag/bagSubstitution.cmo : src/lib/share.cmx src/basic_ag/bag.cmx \
     src/basic_ag/bagSubstitution.cmi
 src/basic_ag/bagSubstitution.cmx : src/lib/share.cmx src/basic_ag/bag.cmx \
     src/basic_ag/bagSubstitution.cmi
-src/basic_ag/bagReduction.cmi : src/common/status.cmx src/basic_ag/bag.cmx
-src/basic_ag/bagReduction.cmo : src/common/status.cmx src/common/options.cmx \
-    src/common/marks.cmi src/lib/log.cmi src/common/entity.cmx \
-    src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
-    src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
-    src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
-src/basic_ag/bagReduction.cmx : src/common/status.cmx src/common/options.cmx \
-    src/common/marks.cmx src/lib/log.cmx src/common/entity.cmx \
-    src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
-    src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
-    src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
-src/basic_ag/bagType.cmi : src/common/status.cmx src/basic_ag/bag.cmx
-src/basic_ag/bagType.cmo : src/common/status.cmx src/lib/share.cmx \
-    src/common/options.cmx src/lib/log.cmi src/common/hierarchy.cmi \
-    src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagReduction.cmi \
-    src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
-    src/basic_ag/bag.cmx src/basic_ag/bagType.cmi
-src/basic_ag/bagType.cmx : src/common/status.cmx src/lib/share.cmx \
-    src/common/options.cmx src/lib/log.cmx src/common/hierarchy.cmx \
-    src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagReduction.cmx \
-    src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
-    src/basic_ag/bag.cmx src/basic_ag/bagType.cmi
-src/basic_ag/bagUntrusted.cmi : src/common/status.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagReduction.cmi : src/common/layer.cmi src/basic_ag/bag.cmx
+src/basic_ag/bagReduction.cmo : src/common/options.cmx src/common/marks.cmi \
+    src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_ag/bagSubstitution.cmi src/basic_ag/bagOutput.cmi \
+    src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
+    src/basic_ag/bagReduction.cmi
+src/basic_ag/bagReduction.cmx : src/common/options.cmx src/common/marks.cmx \
+    src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_ag/bagSubstitution.cmx src/basic_ag/bagOutput.cmx \
+    src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagReduction.cmi
+src/basic_ag/bagType.cmi : src/common/layer.cmi src/basic_ag/bag.cmx
+src/basic_ag/bagType.cmo : src/lib/share.cmx src/common/options.cmx \
+    src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
+    src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
+    src/basic_ag/bagType.cmi
+src/basic_ag/bagType.cmx : src/lib/share.cmx src/common/options.cmx \
+    src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
+    src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagType.cmi
+src/basic_ag/bagUntrusted.cmi : src/common/layer.cmi src/basic_ag/bag.cmx
 src/basic_ag/bagUntrusted.cmo : src/lib/log.cmi src/common/entity.cmx \
     src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \
     src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
@@ -256,8 +252,8 @@ src/basic_ag/bagUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
 src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
     src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \
-    src/text/txt.cmx src/lib/time.cmx src/common/status.cmx \
-    src/common/output.cmi src/common/options.cmx src/lib/log.cmi \
+    src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \
+    src/common/options.cmx src/lib/log.cmi src/common/layer.cmi \
     src/common/hierarchy.cmi src/common/entity.cmx \
     src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
     src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
@@ -270,8 +266,8 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
     src/automath/autCrg.cmi src/automath/aut.cmx
 src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
     src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \
-    src/text/txt.cmx src/lib/time.cmx src/common/status.cmx \
-    src/common/output.cmx src/common/options.cmx src/lib/log.cmx \
+    src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \
+    src/common/options.cmx src/lib/log.cmx src/common/layer.cmx \
     src/common/hierarchy.cmx src/common/entity.cmx \
     src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
     src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 5d359ba39..09dffb04d 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -42,7 +42,7 @@ test-si-matita matita/$(MA): $(MAIN).opt etc
 
 profile: $(MAIN).opt etc
 	@echo "  HELENA -o -q $(INPUTFAST) (30 TIMES)"
-	$(H)rm etc/log.txt
+	$(H)rm -f etc/log.txt
 	$(H)for T in `seq 30`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
 	$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
 
diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common
index 34c521bb6..babfcf50f 100644
--- a/helm/software/helena/Makefile.common
+++ b/helm/software/helena/Makefile.common
@@ -91,6 +91,6 @@ etc:
 	@echo "  OCAMLOPT $<"
 	$(H)$(OCAMLOPT) -c $<
 
-TAGS += $(MAIN).opt
+TAGS += all opt $(MAIN).opt
 
 $(foreach TAG, $(TAGS), $(eval $(call INCLUDE_TEMPLATE, $(TAG))))
diff --git a/helm/software/helena/examples/automath/omega.aut b/helm/software/helena/examples/automath/omega.aut
new file mode 100644
index 000000000..9e6c30e6f
--- /dev/null
+++ b/helm/software/helena/examples/automath/omega.aut
@@ -0,0 +1,8 @@
+# This book is not valid in AUT-QE because [y:'type'] is not allowed
+# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
+# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
+
++l
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+@ Omega := <Delta>Delta : 'type'
+-l
diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 1c2759d15..c38e8532c 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -13,9 +13,8 @@ module U  = NUri
 module UH = U.UriHash
 module C  = Cps
 module G  = Options
-module N  = Level
+module N  = Layer
 module E  = Entity
-module S  = Status
 module A  = Aut
 module D  = Crg
 
@@ -130,7 +129,7 @@ let rec xlate_term f st lst y lenv = function
             let l = if !G.cc then match y, at.E.n_degr with
                | true, _ -> N.one
                | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st.S.lenv
+               | _   , 1 -> N.unknown st
                | _   , 2 -> N.two
                | _       -> assert false
                else N.infinite
diff --git a/helm/software/helena/src/automath/autCrg.mli b/helm/software/helena/src/automath/autCrg.mli
index 9d58247ea..d4e7cef66 100644
--- a/helm/software/helena/src/automath/autCrg.mli
+++ b/helm/software/helena/src/automath/autCrg.mli
@@ -16,4 +16,4 @@ val initial_status: unit -> status
 val refresh_status: status -> status
 
 val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> 
-                Status.status -> status -> Aut.command -> 'a
+                Layer.status -> status -> Aut.command -> 'a
diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
index de74dcb2b..8d35483ea 100644
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -11,7 +11,7 @@
 
 module C = Cps
 module J = Marks
-module N = Level
+module N = Layer
 module E = Entity
 module D = Crg
 module Z = Bag
diff --git a/helm/software/helena/src/basic_ag/bagCrg.mli b/helm/software/helena/src/basic_ag/bagCrg.mli
index b1ffee4af..a46705f78 100644
--- a/helm/software/helena/src/basic_ag/bagCrg.mli
+++ b/helm/software/helena/src/basic_ag/bagCrg.mli
@@ -9,6 +9,6 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val bag_of_crg: Level.status -> (Bag.term -> 'a) -> Crg.term -> 'a
+val bag_of_crg: Layer.status -> (Bag.term -> 'a) -> Crg.term -> 'a
 
 val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a
diff --git a/helm/software/helena/src/basic_ag/bagOutput.mli b/helm/software/helena/src/basic_ag/bagOutput.mli
index 71c388380..64f6b034f 100644
--- a/helm/software/helena/src/basic_ag/bagOutput.mli
+++ b/helm/software/helena/src/basic_ag/bagOutput.mli
@@ -17,6 +17,6 @@ val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
-val specs: (Level.status, Bag.lenv, Bag.term) Log.specs
+val specs: (Layer.status, Bag.lenv, Bag.term) Log.specs
 
-val export_term: Level.status -> Bag.term -> XmlLibrary.pp
+val export_term: Layer.status -> Bag.term -> XmlLibrary.pp
diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index 513c14e59..c9cc85e9b 100644
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -15,7 +15,6 @@ module L  = Log
 module G  = Options
 module J  = Marks
 module E  = Entity
-module S  = Status
 module Z  = Bag
 module ZO = BagOutput
 module ZE = BagEnvironment
@@ -125,7 +124,7 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f st c t =
-   if !G.trace >= level then log1 st.S.lenv "Now scanning" c t;
+   if !G.trace >= level then log1 st "Now scanning" c t;
    ho_whd f c empty_machine t
 
 let rec are_convertible f st a c m1 t1 m2 t2 =
@@ -133,7 +132,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
    let rec aux m1 r1 m2 r2 =
 (*   L.warn "entering R.are_convertible_aux"; *)
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   if !G.trace >= level then log2 st.S.lenv "Now really converting" c u c t;   
+   if !G.trace >= level then log2 st "Now really converting" c u c t;   
    match r1, r2 with
       | Sort_ h1, Sort_ h2                                 ->
          if h1 = h2 then f a else f false 
@@ -166,7 +165,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
          let f r = if r then push "!" h c m1 a1 l w1 else f false in
 	 are_convertible f st a c m1 w1 m2 w2
 (* we detect the AUT-QE reduction rule for type/prop inclusion *)      
-      | Sort_ _, Bind_ (a2, l2, w2, t2) when st.S.si       ->
+      | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si         ->
  	 let m1, m2 = inc m1, inc m2 in
 	 let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
 	 push "nsi" f c m2 a2 l2 w2
@@ -190,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 =
       C.list_fold_left2 f map a m1.s m2.s
 
 let are_convertible f st c u t = 
-   if !G.trace >= level then log2 st.S.lenv "Now converting" c u c t;
+   if !G.trace >= level then log2 st "Now converting" c u c t;
    are_convertible f st true c empty_machine u empty_machine t
diff --git a/helm/software/helena/src/basic_ag/bagReduction.mli b/helm/software/helena/src/basic_ag/bagReduction.mli
index 9a3c849fb..90aa4053b 100644
--- a/helm/software/helena/src/basic_ag/bagReduction.mli
+++ b/helm/software/helena/src/basic_ag/bagReduction.mli
@@ -14,7 +14,7 @@ type ho_whd_result =
    | Abst of Bag.term
 
 val ho_whd: 
-   (ho_whd_result -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> 'a
+   (ho_whd_result -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> 'a
 
 val are_convertible:
-   (bool -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a
+   (bool -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a
diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml
index f8c347892..5585b5d6a 100644
--- a/helm/software/helena/src/basic_ag/bagSubstitution.ml
+++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml
@@ -9,35 +9,35 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module W = Share
+module S = Share
 module Z = Bag
 
 (* Internal functions *******************************************************)
 
 let rec lref_map_bind f map b = match b with
    | Z.Abbr v ->
-      let f v' = f (W.sh1 v v' b Z.abbr) in
+      let f v' = f (S.sh1 v v' b Z.abbr) in
       lref_map f map v      
    | Z.Abst w ->
-      let f w' = f (W.sh1 w w' b Z.abst) in
+      let f w' = f (S.sh1 w w' b Z.abst) in
       lref_map f map w
    | Z.Void   -> f b
 
 and lref_map f map t = match t with
    | Z.LRef i            -> 
-      let ii = map i in f (W.sh1 i ii t Z.lref)
+      let ii = map i in f (S.sh1 i ii t Z.lref)
    | Z.GRef _            -> f t
    | Z.Sort _            -> f t
    | Z.Cast (w, u)       ->
-      let f w' u' = f (W.sh2 w w' u u' t Z.cast) in
+      let f w' u' = f (S.sh2 w w' u u' t Z.cast) in
       let f w' = lref_map (f w') map u in 
       lref_map f map w
    | Z.Appl (w, u)       ->
-      let f w' u' = f (W.sh2 w w' u u' t Z.appl) in
+      let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
       let f w' = lref_map (f w') map u in 
       lref_map f map w
    | Z.Bind (a, l, b, u) ->
-      let f b' u' = f (W.sh2 b b' u u' t (Z.bind a l)) in
+      let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in
       let f b' = lref_map (f b') map u in 
       lref_map_bind f map b
 
diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml
index 33953d6ad..e76399c5f 100644
--- a/helm/software/helena/src/basic_ag/bagType.ml
+++ b/helm/software/helena/src/basic_ag/bagType.ml
@@ -11,12 +11,11 @@
 
 module U  = NUri
 module C  = Cps
-module W  = Share
+module S  = Share
 module L  = Log
 module G  = Options
 module H  = Hierarchy
 module E  = Entity
-module S  = Status
 module Z  = Bag
 module ZO = BagOutput
 module ZE = BagEnvironment
@@ -46,7 +45,7 @@ let mk_gref u l =
 
 let rec b_type_of err f st c x = 
 (*   L.warn "Entering T.b_type_of"; *)
-   if !G.trace >= level then log1 st.S.lenv "Now checking" c x;
+   if !G.trace >= level then log1 st "Now checking" c x;
    match x with
    | Z.Sort h                    ->
       let h = H.apply h in f x (Z.Sort h) 
@@ -69,7 +68,7 @@ let rec b_type_of err f st c x =
       ZE.get_entity f uri   
    | Z.Bind (a, l, Z.Abbr v, t) ->
       let f xv xt tt =
-         f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
+         f (S.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
       in
       let f xv cc = b_type_of err (f xv) st cc t in
       let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
@@ -80,24 +79,24 @@ let rec b_type_of err f st c x =
       type_of err f st c v
    | Z.Bind (a, l, Z.Abst u, t) ->
       let f xu xt tt =
-	 f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
+	 f (S.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
       in
       let f xu cc = b_type_of err (f xu) st cc t in
       let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
       type_of err f st c u
    | Z.Bind (a, l, Z.Void, t)   ->
       let f xt tt = 
-         f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
+         f (S.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
       in
       let f cc = b_type_of err f st cc t in
       Z.push "type void" f c a l Z.Void   
    | Z.Appl (v, t)            ->
       let f xv vv xt tt = function
 	 | ZR.Abst w                             -> 
-	    if !G.trace > level then L.log st.S.lenv ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
+	    if !G.trace > level then L.log st ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
 	    let f a =                
 (*	       L.warn (Printf.sprintf "Convertible: %b" a); *)
-	       if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
+	       if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
 	       else error3 err c xv vv w
 	    in
 	    ZR.are_convertible f st c w vv
@@ -110,7 +109,7 @@ let rec b_type_of err f st c x =
    | Z.Cast (u, t)            ->
       let f xu xt tt a =  
          (* L.warn (Printf.sprintf "Convertible: %b" a); *)
-	 if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu
+	 if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu
       in
       let f xu xt tt = ZR.are_convertible (f xu xt tt) st c xu tt in
       let f xu _ = b_type_of err (f xu) st c t in
diff --git a/helm/software/helena/src/basic_ag/bagType.mli b/helm/software/helena/src/basic_ag/bagType.mli
index 8f343a624..3af585c3f 100644
--- a/helm/software/helena/src/basic_ag/bagType.mli
+++ b/helm/software/helena/src/basic_ag/bagType.mli
@@ -12,4 +12,4 @@
 val type_of: 
    (Bag.message -> 'a) ->
    (Bag.term -> Bag.term -> 'a) ->
-   Status.status -> Bag.lenv -> Bag.term -> 'a
+   Layer.status -> Bag.lenv -> Bag.term -> 'a
diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.mli b/helm/software/helena/src/basic_ag/bagUntrusted.mli
index d9ea41897..c9b0b7c4d 100644
--- a/helm/software/helena/src/basic_ag/bagUntrusted.mli
+++ b/helm/software/helena/src/basic_ag/bagUntrusted.mli
@@ -11,4 +11,4 @@
 
 val type_check:
    (Bag.message -> 'a) -> (Bag.term -> Bag.entity -> 'a) ->
-   Status.status -> Bag.entity -> 'a
+   Layer.status -> Bag.entity -> 'a
diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml
index cdfa93c6e..9cf2f47d2 100644
--- a/helm/software/helena/src/basic_rg/brg.ml
+++ b/helm/software/helena/src/basic_rg/brg.ml
@@ -12,14 +12,14 @@
 (* kernel version: basic, relative, global *)
 (* note          : ufficial basic \lambda\delta *) 
 
-module N = Level
+module N = Layer
 module E = Entity
 
 type uri = E.uri
 type attrs = E.node_attrs
 
 type bind = Void                   (*             *)
-          | Abst of N.level * term (* level, type *)
+          | Abst of N.layer * term (* layer, type *)
           | Abbr of term           (* body        *)
 
 and term = Sort of attrs * int         (* attrs, hierarchy index *)
diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml
index cc1223c0a..0fcde12aa 100644
--- a/helm/software/helena/src/basic_rg/brgCrg.ml
+++ b/helm/software/helena/src/basic_rg/brgCrg.ml
@@ -10,7 +10,7 @@
       V_______________________________________________________________ *)
 
 module C = Cps
-module N = Level
+module N = Layer
 module E = Entity
 module D = Crg
 module B = Brg
diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index 53956d932..cb4935f1e 100644
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -15,7 +15,7 @@ module P = Printf
 module U = NUri
 module C = Cps
 module G = Options
-module N = Level
+module N = Layer
 module E = Entity
 module R = Alpha
 module B = Brg
diff --git a/helm/software/helena/src/basic_rg/brgGrafite.mli b/helm/software/helena/src/basic_rg/brgGrafite.mli
index 27b927773..5b5fca4c5 100644
--- a/helm/software/helena/src/basic_rg/brgGrafite.mli
+++ b/helm/software/helena/src/basic_rg/brgGrafite.mli
@@ -11,6 +11,6 @@
 
 val open_out: string -> out_channel
 
-val output_entity: Level.status -> out_channel -> Brg.entity -> bool
+val output_entity: Layer.status -> out_channel -> Brg.entity -> bool
 
 val close_out: out_channel -> unit
diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml
index 5f2866d24..a49177855 100644
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -16,7 +16,7 @@ module C  = Cps
 module L  = Log
 module G  = Options
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
 module XD = XmlCrg
 module B  = Brg
diff --git a/helm/software/helena/src/basic_rg/brgOutput.mli b/helm/software/helena/src/basic_rg/brgOutput.mli
index 2a603669d..155cc8ee4 100644
--- a/helm/software/helena/src/basic_rg/brgOutput.mli
+++ b/helm/software/helena/src/basic_rg/brgOutput.mli
@@ -17,6 +17,6 @@ val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
-val specs: (Level.status, Brg.lenv, Brg.term) Log.specs
+val specs: (Layer.status, Brg.lenv, Brg.term) Log.specs
 
-val export_term: Level.status -> Brg.term -> XmlLibrary.pp
+val export_term: Layer.status -> Brg.term -> XmlLibrary.pp
diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 7f7dd4e78..002f12ce1 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -10,14 +10,13 @@
       V_______________________________________________________________ *)
 
 module U  = NUri
-module W  = Share
+module S  = Share
 module L  = Log
 module G  = Options
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
 module O  = Output
-module S  = Status
 module B  = Brg
 module BO = BrgOutput
 module BE = BrgEnvironment
@@ -75,7 +74,7 @@ let are_alpha_convertible err f t1 t2 =
       | B.Void, B.Void                                -> f ()
       | _                                             -> err ()
    in
-   if W.eq t1 t2 then f () else aux f (t1, t2)
+   if S.eq t1 t2 then f () else aux f (t1, t2)
 
 let assert_tstep m vo = match m.n with
    | Some n -> n > m.d
@@ -93,7 +92,7 @@ let get m i =
 (* to share *)
 let rec step st m x = 
    if !G.trace >= sublevel then 
-   log1 st.S.lenv (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
+   log1 st (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
    match x with
    | B.Sort (a, h)                ->
       if assert_tstep m false then
@@ -149,10 +148,10 @@ let rec step st m x =
          | []          ->
             let i = tsteps m in
             if i = 0 then m, x, None else
-            let n = N.minus st.S.lenv n i in
+            let n = N.minus st n i in
             m, B.Bind (a, B.Abst (n, w), t), None
 	 | (c, v) :: s ->
-            if !G.cc && not (N.assert_not_zero st.S.lenv n) then assert false;
+            if !G.cc && not (N.assert_not_zero st n) then assert false;
 	    if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
 	    let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
             let e = B.push m.e c a (B.abbr v) in
@@ -179,7 +178,7 @@ let push m a b =
    {m with e = e; l = l}
 
 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
-   if !G.trace >= level then log2 st.S.lenv "Now converting nfs" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _         ->
          h1 = h2
@@ -209,13 +208,13 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
 	 ac_nfs st (step st m1 v1) (m2, t2, r2)
       | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, 
         B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _  ->
-	 if !G.cc && not (N.assert_equal st.S.lenv n1 n2) then false else
-         if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then
+	 if !G.cc && not (N.assert_equal st n1 n2) then false else
+         if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
 	    ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
 	 else false
       | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
-         if st.S.si then
-            if !G.cc && not (N.assert_zero st.S.lenv n) then false else begin
+         if !G.si then
+            if !G.cc && not (N.assert_zero st n) then false else begin
 	    if !G.summary then O.add ~upsilon:1 ();
 	    ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end
          else false
@@ -230,7 +229,7 @@ and ac_stacks st m1 m2 =
    if List.length m1.s <> List.length m2.s then false else
    let map (c1, v1) (c2, v2) =
       let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
-      ac {st with S.si = false} m1 v1 m2 v2
+      ac st m1 v1 m2 v2
    in
    list_and map (m1.s, m2.s)
 
@@ -245,16 +244,16 @@ let get m i =
    let _, _, _, b = B.get m.e i in b
 
 let xwhd st m n t =
-   if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t;   
+   if !G.trace >= level then log1 st "Now scanning" m.e t;   
    let m, t, _ = step st (reset m n) t in
    m, t
 
 let are_convertible st m1 n1 t1 m2 n2 t2 = 
-   if !G.trace >= level then log2 st.S.lenv "Now converting" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
    let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
    r
 (*    let err _ = in 
-      if W.eq mu mw then are_alpha_convertible err f u w else err () *)
+      if S.eq mu mw then are_alpha_convertible err f u w else err () *)
 
 (* error reporting **********************************************************)
 
diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli
index 85df40283..1a2f35007 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.mli
+++ b/helm/software/helena/src/basic_rg/brgReduction.mli
@@ -19,10 +19,10 @@ val get: rtm -> int -> Brg.bind
 
 val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm
 
-val xwhd: Status.status -> rtm -> int option -> Brg.term -> rtm * Brg.term 
+val xwhd: Layer.status -> rtm -> int option -> Brg.term -> rtm * Brg.term 
 
 (* arguments: expected type, inferred type *) 
 val are_convertible: 
-   Status.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool
+   Layer.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool
 
-val specs: (Level.status, rtm, Brg.term) Log.specs
+val specs: (Layer.status, rtm, Brg.term) Log.specs
diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 85a20cbc0..2dfb2552d 100644
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -11,13 +11,12 @@
 
 module U  = NUri
 module C  = Cps
-module W  = Share
+module S  = Share
 module L  = Log
 module G  = Options
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
-module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BS = BrgSubstitution
@@ -66,7 +65,7 @@ let assert_applicability err f st m u w v =
       | _                                -> assert false (**)
 
 let rec b_type_of err f st m x =
-   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
+   if !G.trace >= level then log1 st "Now checking" m x;
    match x with
    | B.Sort (a, h)           ->
       let h = H.apply h in f x (B.Sort (a, h)) 
@@ -90,7 +89,7 @@ let rec b_type_of err f st m x =
       end
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv m = b_type_of err (f xv) st m t in
       let f xv = f xv (BR.push m a (B.abbr xv)) in
@@ -101,27 +100,27 @@ let rec b_type_of err f st m x =
       type_of err f st m v
    | B.Bind (a, B.Abst (n, u), t) ->
       let f xu xt tt =
-	 f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st.S.lenv n 1) a xu tt)
+	 f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st n 1) a xu tt)
       in
       let f xu m = b_type_of err (f xu) st m t in
       let f xu _ = f xu (BR.push m a (B.abst n xu)) in
       type_of err f st m u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+         f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
       in
       b_type_of err f st (BR.push m a B.Void) t
          
    | B.Appl (a, v, t)        ->
       let f xv vv xt tt = 
-         let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+         let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
          assert_applicability err f st m tt vv xv
       in
       let f xv vv = b_type_of err (f xv vv) st m t in
       type_of err f st m v
    | B.Cast (a, u, t)        ->
       let f xu xt tt =  
-	 let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
+	 let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
          assert_convertibility err f st m xu tt xt
       in
       let f xu _ = b_type_of err (f xu) st m t in
diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli
index f68259a6e..2a2442097 100644
--- a/helm/software/helena/src/basic_rg/brgType.mli
+++ b/helm/software/helena/src/basic_rg/brgType.mli
@@ -11,4 +11,4 @@
 
 val type_of: 
    (BrgReduction.message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> 
-   Status.status -> BrgReduction.rtm -> Brg.term -> 'a
+   Layer.status -> BrgReduction.rtm -> Brg.term -> 'a
diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.mli b/helm/software/helena/src/basic_rg/brgUntrusted.mli
index a93abd5b6..f3c34ab14 100644
--- a/helm/software/helena/src/basic_rg/brgUntrusted.mli
+++ b/helm/software/helena/src/basic_rg/brgUntrusted.mli
@@ -11,8 +11,8 @@
 
 val type_check:
    (BrgReduction.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> 
-   Status.status -> Brg.entity -> 'a
+   Layer.status -> Brg.entity -> 'a
 
 val validate:
    (BrgReduction.message -> 'a) -> (unit -> 'a) -> 
-   Status.status -> Brg.entity -> 'a
+   Layer.status -> Brg.entity -> 'a
diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index ea3ce2f42..458962b1f 100644
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -12,7 +12,6 @@
 module L  = Log
 module G  = Options
 module E  = Entity
-module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
@@ -62,7 +61,7 @@ let assert_applicability err f st m v t =
       | _                                -> assert false (**)
 
 let rec b_validate err f st m x =
-   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
+   if !G.trace >= level then log1 st "Now checking" m x;
    match x with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->
diff --git a/helm/software/helena/src/basic_rg/brgValidity.mli b/helm/software/helena/src/basic_rg/brgValidity.mli
index 1b552b83c..fca8589ab 100644
--- a/helm/software/helena/src/basic_rg/brgValidity.mli
+++ b/helm/software/helena/src/basic_rg/brgValidity.mli
@@ -11,4 +11,4 @@
 
 val validate: 
    (BrgReduction.message -> 'a) -> (unit -> 'a) -> 
-   Status.status -> BrgReduction.rtm -> Brg.term -> 'a
+   Layer.status -> BrgReduction.rtm -> Brg.term -> 'a
diff --git a/helm/software/helena/src/common/Make b/helm/software/helena/src/common/Make
index 5ccf50d11..c019e1d23 100644
--- a/helm/software/helena/src/common/Make
+++ b/helm/software/helena/src/common/Make
@@ -1 +1 @@
-options marks hierarchy level entity output alpha status 
+options marks hierarchy layer entity output alpha
diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml
index d4bfef5d3..c53db162b 100644
--- a/helm/software/helena/src/common/entity.ml
+++ b/helm/software/helena/src/common/entity.ml
@@ -10,7 +10,7 @@
       V_______________________________________________________________ *)
 
 module U = NUri
-module N = Level
+module N = Layer
 
 type uri = U.uri
 
diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
new file mode 100644
index 000000000..61254620f
--- /dev/null
+++ b/helm/software/helena/src/common/layer.ml
@@ -0,0 +1,187 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module H = Hashtbl
+
+module L = Log
+module G = Options
+module J = Marks
+
+type value = Inf                 (* infinite layer *)
+           | Fin of int          (* finite layer *)
+           | Ref of J.mark * int (* referred layer, step *)
+           | Unk                 (* no layer set *)
+
+type layer = {
+  mutable v: value; (* value *)  
+          s: bool;  (* static layer? *)
+  mutable b: bool;  (* beta allowed? *)
+}
+
+type status = (J.mark, layer) H.t (* environment for layer variables *)
+
+(* Internal functions *******************************************************)
+
+let level = 6
+
+let env_size = 1300
+
+let zero = Fin 0
+
+let warn s = L.warn level s
+
+let string_of_value k = function
+   | Inf        -> ""
+   | Fin i      -> string_of_int i
+   | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
+   | Unk        -> "-" ^ J.string_of_mark k
+
+let pp_table st =
+   let map k n =
+      warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
+         (J.string_of_mark k) (string_of_value k n.v) n.s n.b
+      )
+   in
+   H.iter map st 
+
+let cell s v = {
+   v = v; s = s; b = false
+}
+
+let empty () = cell true Unk
+
+let dynamic k i = cell false (Ref (k, i))
+
+let find_with_default st default k =
+   try H.find st k with Not_found -> H.add st k default; default 
+
+let find st k =
+   try H.find st k with Not_found -> assert false 
+
+let rec resolve_key_with_default st default k = match find_with_default st default k with
+   | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
+   | cell                        -> k, cell
+
+let rec resolve_key st k = match find st k with
+   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
+   | cell                        -> k, cell
+
+let resolve_layer st = function
+   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
+   | cell                        -> J.null_mark, cell
+
+let rec generated st h i =
+   let default = dynamic h i in
+   let k = J.new_mark () in
+   match resolve_key_with_default st default k with
+      | k, n when n = default   -> if !G.trace >= level then pp_table st; n
+      | _, n when n.s = true -> generated st h i
+      | _                    -> assert false
+
+let assert_finite st n j =
+   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+   let rec aux (k, n) j = match n.v with    
+      | Fin i when i = j -> true
+      | Fin i            ->
+         Printf.printf "binder %s is %u but must be %u\n" (J.string_of_mark k) i j; true (**)
+      | Inf              ->
+         Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**)
+      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+      | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
+   in
+   let k, n = resolve_layer st n in
+(*   if j = 0 && n.b then begin
+      Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
+   end else *)
+      aux (k, n) j
+
+let assert_infinite st n =
+   if !G.trace >= level then warn "ASSERT INFINITE";
+   let rec aux (k, n) = match n.v with
+      | Inf        -> true
+      | Fin i      -> 
+         Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**)
+      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+      | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
+   in
+   aux (resolve_layer st n)
+
+(* Interface functions ******************************************************)
+
+let initial_status () =
+   H.create env_size
+
+let refresh_status st = st 
+
+let infinite = cell true Inf
+
+let finite i = cell true (Fin i)
+
+let one = finite 1
+
+let two = finite 2
+
+let rec unknown st =
+   if !G.trace >= level then warn "UNKNOWN";
+   let default = empty () in
+   let k = J.new_mark () in
+   match resolve_key_with_default st default k with
+      | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | _, n when n.s = true  -> n
+      | _                     -> unknown st
+
+let minus st n j =
+   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+   let rec aux k n j = match n.v with
+      | Inf              -> cell false n.v
+      | Fin i when i > j -> cell false (Fin (i - j))
+      | Fin _            -> cell false zero
+      | Unk              ->
+         if k = J.null_mark then assert false else generated st k j
+      | Ref (k, i)       -> 
+         let k, n = resolve_key st k in
+         aux k n (i+j)      
+   in
+   let k, n = resolve_layer st n in
+   aux k n j
+
+let to_string st n =
+   let k, n = resolve_layer st n in
+   string_of_value k n.v
+
+let assert_not_zero st n =
+   if !G.trace >= level then warn "ASSERT NOT ZERO";
+   let k, n = resolve_layer st n in
+   match n.b, n.v with
+      | true, _                -> n.b
+(*      | _   , Fin i when i = 0 ->   
+         Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**)
+(*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *)      
+      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+
+let assert_zero st n = assert_finite st n 0
+
+let assert_equal st n1 n2 =
+   let k1, n1 = resolve_layer st n1 in
+   let k2, n2 = resolve_layer st n2 in
+   if n1 = n2 then true else
+   let b =
+      if not n1.b || assert_not_zero st n2 then match n1.v with
+         | Inf   -> assert_infinite st n2
+         | Fin i -> assert_finite st n2 i
+         | Unk   -> true
+         | Ref _ -> assert false
+      else false
+   in begin
+   if !G.trace >= level then warn "ASSERT EQUAL";
+   if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
+      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
+   end; b end
diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli
new file mode 100644
index 000000000..9d8b34e72
--- /dev/null
+++ b/helm/software/helena/src/common/layer.mli
@@ -0,0 +1,38 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+type status
+
+type layer
+
+val initial_status: unit -> status
+
+val refresh_status: status -> status
+
+val infinite: layer
+
+val finite: int -> layer
+
+val one: layer
+
+val two: layer
+
+val unknown: status -> layer
+
+val minus: status -> layer -> int -> layer
+
+val to_string: status -> layer -> string
+
+val assert_not_zero: status -> layer -> bool
+
+val assert_zero: status -> layer -> bool
+
+val assert_equal: status -> layer -> layer -> bool
diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml
deleted file mode 100644
index 5f5251f6c..000000000
--- a/helm/software/helena/src/common/level.ml
+++ /dev/null
@@ -1,185 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module H = Hashtbl
-
-module L = Log
-module G = Options
-module J = Marks
-
-type value = Inf                 (* infinite level *)
-           | Fin of int          (* finite level *)
-           | Ref of J.mark * int (* referred level, step *)
-           | Unk                 (* no level set *)
-
-type level = {
-  mutable v: value; (* value *)  
-          s: bool;  (* static level? *)
-  mutable b: bool;  (* beta allowed? *)
-}
-
-type status = (J.mark, level) H.t (* environment for level variables *)
-
-(* Internal functions *******************************************************)
-
-let level = 6
-
-let env_size = 1300
-
-let zero = Fin 0
-
-let warn s = L.warn level s
-
-let string_of_value k = function
-   | Inf        -> ""
-   | Fin i      -> string_of_int i
-   | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
-   | Unk        -> "-" ^ J.string_of_mark k
-
-let pp_table st =
-   let map k n =
-      warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
-         (J.string_of_mark k) (string_of_value k n.v) n.s n.b
-      )
-   in
-   H.iter map st 
-
-let cell s v = {
-   v = v; s = s; b = false
-}
-
-let empty () = cell true Unk
-
-let dynamic k i = cell false (Ref (k, i))
-
-let find_with_default st default k =
-   try H.find st k with Not_found -> H.add st k default; default 
-
-let find st k =
-   try H.find st k with Not_found -> assert false 
-
-let rec resolve_key_with_default st default k = match find_with_default st default k with
-   | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
-   | cell                        -> k, cell
-
-let rec resolve_key st k = match find st k with
-   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
-   | cell                        -> k, cell
-
-let resolve_level st = function
-   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
-   | cell                        -> J.null_mark, cell
-
-let rec generated st h i =
-   let default = dynamic h i in
-   let k = J.new_mark () in
-   match resolve_key_with_default st default k with
-      | k, n when n = default   -> if !G.trace >= level then pp_table st; n
-      | _, n when n.s = true -> generated st h i
-      | _                    -> assert false
-
-let assert_finite st n j =
-   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
-   let rec aux (k, n) j = match n.v with    
-      | Fin i when i = j -> true
-      | Fin i            ->
-         Printf.printf "binder %s is %u but must be %u\n" (J.string_of_mark k) i j; true (**)
-      | Inf              ->
-         Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**)
-      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
-      | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
-   in
-   let k, n = resolve_level st n in
-(*   if j = 0 && n.b then begin
-      Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
-   end else *)
-      aux (k, n) j
-
-let assert_infinite st n =
-   if !G.trace >= level then warn "ASSERT INFINITE";
-   let rec aux (k, n) = match n.v with
-      | Inf        -> true
-      | Fin i      -> 
-         Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**)
-      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
-      | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
-   in
-   aux (resolve_level st n)
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
-   H.create env_size
-
-let infinite = cell true Inf
-
-let finite i = cell true (Fin i)
-
-let one = finite 1
-
-let two = finite 2
-
-let rec unknown st =
-   if !G.trace >= level then warn "UNKNOWN";
-   let default = empty () in
-   let k = J.new_mark () in
-   match resolve_key_with_default st default k with
-      | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
-      | _, n when n.s = true  -> n
-      | _                     -> unknown st
-
-let minus st n j =
-   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
-   let rec aux k n j = match n.v with
-      | Inf              -> cell false n.v
-      | Fin i when i > j -> cell false (Fin (i - j))
-      | Fin _            -> cell false zero
-      | Unk              ->
-         if k = J.null_mark then assert false else generated st k j
-      | Ref (k, i)       -> 
-         let k, n = resolve_key st k in
-         aux k n (i+j)      
-   in
-   let k, n = resolve_level st n in
-   aux k n j
-
-let to_string st n =
-   let k, n = resolve_level st n in
-   string_of_value k n.v
-
-let assert_not_zero st n =
-   if !G.trace >= level then warn "ASSERT NOT ZERO";
-   let k, n = resolve_level st n in
-   match n.b, n.v with
-      | true, _                -> n.b
-(*      | _   , Fin i when i = 0 ->   
-         Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**)
-(*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *)      
-      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
-
-let assert_zero st n = assert_finite st n 0
-
-let assert_equal st n1 n2 =
-   let k1, n1 = resolve_level st n1 in
-   let k2, n2 = resolve_level st n2 in
-   if n1 = n2 then true else
-   let b =
-      if not n1.b || assert_not_zero st n2 then match n1.v with
-         | Inf   -> assert_infinite st n2
-         | Fin i -> assert_finite st n2 i
-         | Unk   -> true
-         | Ref _ -> assert false
-      else false
-   in begin
-   if !G.trace >= level then warn "ASSERT EQUAL";
-   if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
-      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
-   end; b end
diff --git a/helm/software/helena/src/common/level.mli b/helm/software/helena/src/common/level.mli
deleted file mode 100644
index fe12b3671..000000000
--- a/helm/software/helena/src/common/level.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-type status
-
-type level
-
-val initial_status: unit -> status
-
-val infinite: level
-
-val finite: int -> level
-
-val one: level
-
-val two: level
-
-val unknown: status -> level
-
-val minus: status -> level -> int -> level
-
-val to_string: status -> level -> string
-
-val assert_not_zero: status -> level -> bool
-
-val assert_zero: status -> level -> bool
-
-val assert_equal: status -> level -> level -> bool
diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml
deleted file mode 100644
index 401faf9af..000000000
--- a/helm/software/helena/src/common/status.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module G = Options
-module N = Level
-
-type status = {
-   si: bool;       (* sort inclusion *)
-   lenv: N.status; (* level environment *)
-}
-
-(* helpers ******************************************************************)
-
-let initial_status () = {
-   si = !G.si; lenv = N.initial_status ();
-}
-
-let refresh_status st = {st with
-   si = !G.si (*; lenv = N.initial_status (); *)
-}
diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index 87fbaf3e2..673b3a0ba 100644
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -13,14 +13,14 @@
 (* note          : fragment of complete \lambda\delta serving as abstract layer *) 
 
 module C = Cps
-module N = Level
+module N = Layer
 module E = Entity
 
 type uri = E.uri
 type id = E.id
 type attrs = E.node_attrs
 
-type bind = Abst of N.level * term      (* level, type *)
+type bind = Abst of N.layer * term      (* layer, type *)
           | Abbr of term                (* body *)
           | Void                        (* *)
 
diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index dfef1f250..6ccf47af0 100644
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -15,7 +15,7 @@ module U = NUri
 module C = Cps
 module L = Log
 module J = Marks
-module N = Level
+module N = Layer
 module E = Entity
 module D = Crg
 
diff --git a/helm/software/helena/src/complete_rg/crgOutput.mli b/helm/software/helena/src/complete_rg/crgOutput.mli
index b0a4c718c..a3f636381 100644
--- a/helm/software/helena/src/complete_rg/crgOutput.mli
+++ b/helm/software/helena/src/complete_rg/crgOutput.mli
@@ -17,4 +17,4 @@ val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
-val pp_term: (string -> unit) -> Level.status -> Crg.term -> unit
+val pp_term: (string -> unit) -> Layer.status -> Crg.term -> unit
diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml
index 07709401c..834a9a19f 100644
--- a/helm/software/helena/src/modules.ml
+++ b/helm/software/helena/src/modules.ml
@@ -1,21 +1,20 @@
-(* free = F I K M P Q U V *)
+(* free = F I K M P Q U V W *)
 
 module U  = NUri
 module UH = NUri.UriHash
 
 module C  = Cps
-module W  = Share (**)
+module S  = Share
 module L  = Log
 module Y  = Time (**)
 
 module G  = Options
 module J  = Marks (**)
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
 module O  = Output
 module R  = Alpha
-module S  = Status
 
 module D  = Crg
 module DO = CrgOutput
diff --git a/helm/software/helena/src/text/txt.ml b/helm/software/helena/src/text/txt.ml
index bdd96bf6b..0633d39a9 100644
--- a/helm/software/helena/src/text/txt.ml
+++ b/helm/software/helena/src/text/txt.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module N = Level
+module N = Layer
 
 type ix = int (* index *)
 
@@ -45,11 +45,11 @@ and term =
 (* arguments, function *)
 	 | Appl of term list * term
 (* level, binder, scope *)
-	 | Bind of N.level * bind * term
+	 | Bind of N.layer * bind * term
 (* function, arguments *)
 	 | Inst of term * term list
 (* level, strong?, label, source, target *)
-	 | Impl of N.level * bool * id * term * term
+	 | Impl of N.layer * bool * id * term * term
 
 type command =
 (* required files: names *)
@@ -61,6 +61,6 @@ type command =
 (* section: Some id = open, None = close last *)
 	     | Section of id option
 (* entity: main?, class, name, info, contents *)
-	     | Entity of bool * kind * N.level * id * info * term
+	     | Entity of bool * kind * N.layer * id * info * term
 (* predefined generated entity: arguments *)
              | Generate of term list
diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly
index 2c9abe079..d9336b189 100644
--- a/helm/software/helena/src/text/txtParser.mly
+++ b/helm/software/helena/src/text/txtParser.mly
@@ -25,7 +25,7 @@
 
 %{
    module G = Options
-   module N = Level
+   module N = Layer
    module T = Txt
    
    let _ = Parsing.set_trace !G.debug_parser
diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 535450c1f..bded35b3b 100644
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -18,9 +18,9 @@ module L  = Log
 module Y  = Time
 module G  = Options
 module H  = Hierarchy
+module N  = Layer
 module E  = Entity
 module O  = Output
-module S  = Status
 module DO = CrgOutput
 module TD = TxtCrg
 module AA = AutProcess
@@ -39,7 +39,7 @@ module ZT = BagType
 module ZU = BagUntrusted
 
 type status = {
-   kst: S.status;
+   kst: N.status;
    tst: TD.status;
    pst: AA.status;
    ast: AD.status;
@@ -53,13 +53,13 @@ type status = {
 let level = 0
 
 let bag_error st s msg =
-   L.error st.kst.S.lenv ZO.specs (L.Warn s :: msg) 
+   L.error st.kst ZO.specs (L.Warn s :: msg) 
 
 let brg_error st s msg =
-   L.error st.kst.S.lenv BR.specs (L.Warn s :: msg)
+   L.error st.kst BR.specs (L.Warn s :: msg)
 
 let initial_status () = {
-   kst = S.initial_status ();
+   kst = N.initial_status ();
    tst = TD.initial_status ();
    pst = AA.initial_status ();
    ast = AD.initial_status ();
@@ -71,7 +71,7 @@ let initial_status () = {
 }
 
 let refresh_status st = {st with
-   kst = S.refresh_status st.kst;
+   kst = N.refresh_status st.kst;
    tst = TD.refresh_status st.tst;
    ast = AD.refresh_status st.ast;
 }
@@ -91,7 +91,7 @@ let xlate_entity st entity = match !G.kernel, entity with
    | G.Brg, CrgEntity e -> 
       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
    | G.Bag, CrgEntity e -> 
-      let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst.S.lenv) e
+      let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e
    | _, entity          -> entity
 
 let pp_progress e =
@@ -110,9 +110,9 @@ let count_entity st = function
    | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
 
 let export_entity st = function
-   | CrgEntity e -> XL.export_entity (XD.export_term st.kst.S.lenv) e
-   | BrgEntity e -> XL.export_entity (BO.export_term st.kst.S.lenv) e
-   | BagEntity e -> XL.export_entity (ZO.export_term st.kst.S.lenv) e
+   | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e
+   | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e
+   | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e
 
 let type_check st k =
    let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in
@@ -132,7 +132,7 @@ let validate st k =
          begin match st.och with
             | None     -> st
             | Some och -> 
-               if BG.output_entity st.kst.S.lenv och entity then st
+               if BG.output_entity st.kst och entity then st
                else begin L.warn level "Matita exportation stopped"; {st with och = None} end
          end
       | BagEntity _      -> st
diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index 311a0b4a1..535682143 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -81,7 +81,7 @@ and exp_appl st e a v out tab =
 
 and exp_bind st e a b out tab = match b with
    | D.Abst (n, w) ->
-      let attrs = [XL.level st n; XL.name a; XL.kind a] in
+      let attrs = [XL.layer st n; XL.name a; XL.kind 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/xmlCrg.mli b/helm/software/helena/src/xml/xmlCrg.mli
index f1f5e131d..63a9f6800 100644
--- a/helm/software/helena/src/xml/xmlCrg.mli
+++ b/helm/software/helena/src/xml/xmlCrg.mli
@@ -9,4 +9,4 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val export_term: Level.status -> Crg.term -> XmlLibrary.pp
+val export_term: Layer.status -> Crg.term -> XmlLibrary.pp
diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 4caa7c1c2..77fb9351a 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -15,7 +15,7 @@ module U = NUri
 module C = Cps
 module G = Options
 module H = Hierarchy
-module N = Level
+module N = Layer
 module E = Entity
 
 (* internal functions *******************************************************)
@@ -99,8 +99,8 @@ let name a =
 let apix a =
    "position", string_of_int a.E.n_apix
 
-let level st n =
-   "level", N.to_string st n
+let layer st n =
+   "layer", N.to_string st n
 
 let kind a =
    "position", string_of_int a.E.n_sort
diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli
index 1ac861aee..ed7901f57 100644
--- a/helm/software/helena/src/xml/xmlLibrary.mli
+++ b/helm/software/helena/src/xml/xmlLibrary.mli
@@ -41,7 +41,7 @@ val position: int -> attr
 
 val uri: Entity.uri -> attr
 
-val level: Level.status -> Level.level -> attr
+val layer: Layer.status -> Layer.layer -> attr
 
 val name: Entity.node_attrs -> attr