- we removed a flag from the kernel status

- some renaming

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index 016521236d6e046074eef0cf661b60d31aa2ff2b..0580e6bfce3f6c6c2e11c5f0600511d412251179 100644 (file)
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -1,257 +1,260 @@
-src/lib/cps.cmo:
-src/lib/cps.cmx:
-src/lib/share.cmo:
-src/lib/share.cmx:
-src/lib/log.cmi:
-src/lib/log.cmo: src/lib/log.cmi
-src/lib/log.cmx: src/lib/log.cmi
-src/lib/time.cmo: src/lib/log.cmi
-src/lib/time.cmx: src/lib/log.cmx
-src/common/options.cmo: src/lib/cps.cmx
-src/common/options.cmx: src/lib/cps.cmx
-src/common/marks.cmi:
-src/common/marks.cmo: src/common/marks.cmi
-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/cps.cmo :
+src/lib/cps.cmx :
+src/lib/share.cmo :
+src/lib/share.cmx :
+src/lib/log.cmi :
+src/lib/log.cmo : src/lib/log.cmi
+src/lib/log.cmx : src/lib/log.cmi
+src/lib/time.cmo : src/lib/log.cmi
+src/lib/time.cmx : src/lib/log.cmx
+src/common/options.cmo : src/lib/cps.cmx
+src/common/options.cmx : src/lib/cps.cmx
+src/common/marks.cmi :
+src/common/marks.cmo : src/common/marks.cmi
+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/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/output.cmi:
-src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \
+src/common/entity.cmo : src/common/level.cmi
+src/common/entity.cmx : src/common/level.cmx
+src/common/output.cmi :
+src/common/output.cmo : src/common/options.cmx src/lib/log.cmi \
     src/common/output.cmi
-src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
+src/common/output.cmx : src/common/options.cmx src/lib/log.cmx \
     src/common/output.cmi
-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/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/lib/cps.cmx
-src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \
+src/complete_rg/crg.cmx : src/common/level.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.cmo: src/common/marks.cmi src/lib/log.cmi \
+src/complete_rg/crgOutput.cmi : src/common/level.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/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx: src/common/marks.cmx src/lib/log.cmx \
+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/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/txtParser.cmi: src/text/txt.cmx
-src/text/txtParser.cmo: src/text/txt.cmx src/common/options.cmx \
+src/text/txt.cmo : src/common/level.cmi
+src/text/txt.cmx : src/common/level.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/text/txtParser.cmx: src/text/txt.cmx src/common/options.cmx \
+src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \
     src/common/level.cmx src/text/txtParser.cmi
-src/text/txtLexer.cmo: src/text/txtParser.cmi src/common/options.cmx \
+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 \
+src/text/txtLexer.cmx : src/text/txtParser.cmx src/common/options.cmx \
     src/lib/log.cmx
-src/text/txtTxt.cmi: src/text/txt.cmx
-src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
-src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
-src/text/txtCrg.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
-src/text/txtCrg.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
+src/text/txtTxt.cmi : src/text/txt.cmx
+src/text/txtTxt.cmo : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
+src/text/txtTxt.cmx : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
+src/text/txtCrg.cmi : src/text/txt.cmx src/complete_rg/crg.cmx
+src/text/txtCrg.cmo : src/text/txtTxt.cmi src/text/txt.cmx \
     src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
     src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
-src/text/txtCrg.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
+src/text/txtCrg.cmx : src/text/txtTxt.cmx src/text/txt.cmx \
     src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
     src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
-src/automath/aut.cmo: src/common/entity.cmx
-src/automath/aut.cmx: src/common/entity.cmx
-src/automath/autProcess.cmi: src/automath/aut.cmx
-src/automath/autProcess.cmo: src/automath/aut.cmx src/automath/autProcess.cmi
-src/automath/autProcess.cmx: src/automath/aut.cmx src/automath/autProcess.cmi
-src/automath/autOutput.cmi: src/automath/autProcess.cmi src/automath/aut.cmx
-src/automath/autOutput.cmo: src/lib/log.cmi src/lib/cps.cmx \
+src/automath/aut.cmo : src/common/entity.cmx
+src/automath/aut.cmx : src/common/entity.cmx
+src/automath/autProcess.cmi : src/automath/aut.cmx
+src/automath/autProcess.cmo : src/automath/aut.cmx \
+    src/automath/autProcess.cmi
+src/automath/autProcess.cmx : src/automath/aut.cmx \
+    src/automath/autProcess.cmi
+src/automath/autOutput.cmi : src/automath/autProcess.cmi \
+    src/automath/aut.cmx
+src/automath/autOutput.cmo : src/lib/log.cmi src/lib/cps.cmx \
     src/automath/autProcess.cmi src/automath/aut.cmx \
     src/automath/autOutput.cmi
-src/automath/autOutput.cmx: src/lib/log.cmx src/lib/cps.cmx \
+src/automath/autOutput.cmx : src/lib/log.cmx src/lib/cps.cmx \
     src/automath/autProcess.cmx src/automath/aut.cmx \
     src/automath/autOutput.cmi
-src/automath/autParser.cmi: src/automath/aut.cmx
-src/automath/autParser.cmo: src/common/options.cmx src/automath/aut.cmx \
+src/automath/autParser.cmi : src/automath/aut.cmx
+src/automath/autParser.cmo : src/common/options.cmx src/automath/aut.cmx \
     src/automath/autParser.cmi
-src/automath/autParser.cmx: src/common/options.cmx src/automath/aut.cmx \
+src/automath/autParser.cmx : src/common/options.cmx src/automath/aut.cmx \
     src/automath/autParser.cmi
-src/automath/autLexer.cmo: src/common/options.cmx src/lib/log.cmi \
+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/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/status.cmx src/complete_rg/crg.cmx \
     src/automath/aut.cmx
-src/automath/autCrg.cmo: src/common/status.cmx src/common/options.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/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/xml/xmlLibrary.cmi : src/common/level.cmi src/common/entity.cmx
+src/xml/xmlLibrary.cmo : src/common/options.cmx src/common/level.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/level.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/level.cmi \
     src/complete_rg/crg.cmx
-src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
+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 \
     src/common/alpha.cmi src/xml/xmlCrg.cmi
-src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \
+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/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/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/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/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/level.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/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \
     src/common/level.cmi src/basic_rg/brg.cmx
-src/basic_rg/brgOutput.cmo: src/xml/xmlCrg.cmi src/common/options.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/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/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/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
-src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx \
+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.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
-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/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
+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/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/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/brgValidity.cmi : src/common/status.cmx \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
-src/basic_rg/brgValidity.cmo: src/common/status.cmx src/common/options.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/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/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/brgEnvironment.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgValidity.cmi
-src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \
-    src/basic_rg/brg.cmx
-src/basic_rg/brgType.cmo: src/common/status.cmx src/lib/share.cmx \
+src/basic_rg/brgType.cmi : src/common/status.cmx \
+    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/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/brgUntrusted.cmi : src/common/status.cmx \
     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/brgUntrusted.cmo : src/lib/log.cmi src/common/entity.cmx \
     src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi \
     src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
-src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
+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/level.cmi src/basic_rg/brg.cmx
+src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/level.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/level.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/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/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/level.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/level.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/level.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/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \
     src/common/level.cmi src/basic_ag/bag.cmx
-src/basic_ag/bagOutput.cmo: src/xml/xmlCrg.cmi src/common/options.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 \
     src/basic_ag/bagOutput.cmi
-src/basic_ag/bagOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \
+src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \
     src/common/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \
     src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \
     src/basic_ag/bagOutput.cmi
-src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx
-src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \
+src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx
+src/basic_ag/bagEnvironment.cmo : src/lib/log.cmi src/common/entity.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \
+src/basic_ag/bagEnvironment.cmx : src/lib/log.cmx src/common/entity.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagSubstitution.cmi: src/common/marks.cmi src/basic_ag/bag.cmx
-src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \
+src/basic_ag/bagSubstitution.cmi : src/common/marks.cmi src/basic_ag/bag.cmx
+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.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/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/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/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/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/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
+src/basic_ag/bagUntrusted.cmi : src/common/status.cmx 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
-src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
+src/basic_ag/bagUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \
     src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
     src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
-src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.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 \
@@ -265,7 +268,7 @@ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
     src/automath/autProcess.cmi src/automath/autParser.cmi \
     src/automath/autOutput.cmi src/automath/autLexer.cmx \
     src/automath/autCrg.cmi src/automath/aut.cmx
-src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.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 \

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 1fd77cd5140b3cdaf7fb1638244fff726dc5b36b..7f7dd4e788e6d64fac9f416f0b959e28378b5363 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -22,7 +22,7 @@ module B  = Brg
 module BO = BrgOutput
 module BE = BrgEnvironment
 
-type kam = {
+type rtm = {
    e: B.lenv;                 (* environment              *)
    s: (B.lenv * B.term) list; (* stack                    *)
    l: int;                    (* level                    *)
@@ -30,7 +30,7 @@ type kam = {
    n: int option;             (* expected type iterations *)
 }
 
-type message = (kam, B.term) L.message
+type message = (rtm, B.term) L.message
 
 (* Internal functions *******************************************************)
 
@@ -102,7 +102,7 @@ let rec step st m x =
    | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abbr v ->
-            if st.S.delta then begin
+            if m.n = None || !G.expand then begin
               if !G.summary then O.add ~gdelta:1 ();
                step st m v
             end else
@@ -141,7 +141,11 @@ let rec step st m x =
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
-      begin match m.s with
+(*      if not !G.cc && st.S.si && N.to_string st.S.lenv n = "0" then begin
+         if !G.summary then O.add ~upsilon:1 ();
+         let e = B.push m.e m.e a B.Void in 
+         step st {m with e = e} t
+      end else *) begin match m.s with
          | []          ->
             let i = tsteps m in
             if i = 0 then m, x, None else
@@ -169,7 +173,7 @@ let assert_iterations m1 m2 = match m1.n, m2.n with
 let push m a b = 
    let a, l = match b with
       | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
-      | b        -> a, m.l
+      | _        -> a, m.l
    in
    let e = B.push m.e m.e a b in
    {m with e = e; l = l}
@@ -177,15 +181,15 @@ let push m a b =
 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;
    match t1, r1, t2, r2 with
-      | B.Sort (_, h1), _, B.Sort (_, h2), _                ->
+      | B.Sort (_, h1), _, B.Sort (_, h2), _         ->
          h1 = h2
       | B.LRef ({E.n_apix = e1}, _), _, 
-        B.LRef ({E.n_apix = e2}, _), _                      ->
+        B.LRef ({E.n_apix = e2}, _), _               ->
         if e1 = e2 then ac_stacks st m1 m2 else false
-      | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
+      | B.GRef (_, u1), None, B.GRef (_, u2), None   ->
         if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
       | B.GRef ({E.n_apix = e1}, u1), Some v1, 
-        B.GRef ({E.n_apix = e2}, u2), Some v2               ->
+        B.GRef ({E.n_apix = e2}, u2), Some v2        ->
          if e1 < e2 then begin 
             if !G.summary then O.add ~gdelta:1 ();
            ac_nfs st (m1, t1, r1) (step st m2 v2)
@@ -197,25 +201,25 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
            if !G.summary then O.add ~gdelta:2 ();
            ac st m1 v1 m2 v2
          end 
-      | _, _, B.GRef _, Some v2                             ->
+      | _, _, B.GRef _, Some v2                      ->
          if !G.summary then O.add ~gdelta:1 ();
         ac_nfs st (m1, t1, r1) (step st m2 v2)
-      | B.GRef _, Some v1, _, _                             ->
+      | B.GRef _, Some v1, _, _                      ->
         if !G.summary then O.add ~gdelta:1 ();
         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), _         ->
+        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
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
-      | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
+      | 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.summary then O.add ~si:1 ();
-           ac st (push m1 a b) t1 (push m2 a b) t end
+           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
-      | _                                                   -> false
+      | _                                            -> false
 
 and ac st m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)
@@ -232,7 +236,7 @@ and ac_stacks st m1 m2 =
 
 (* Interface functions ******************************************************)
 
-let empty_kam = { 
+let empty_rtm = { 
    e = B.empty; s = []; l = 0; d = 0; n = None
 }
 
@@ -242,12 +246,12 @@ let get m i =
 
 let xwhd st m n t =
    if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t;   
-   let m, t, _ = step {st with S.delta = true} (reset m n) t in
+   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;
-   let r = ac {st with S.delta = !G.expand} (reset m1 n1) t1 (reset m2 n2) t2 in
+   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 () *)

diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli
index 42798aeee066437b1d86061bc1c51953a066708b..85df402838562175f3354d4c3177fee99c60d7cf 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.mli
+++ b/helm/software/helena/src/basic_rg/brgReduction.mli
@@ -9,20 +9,20 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-type kam
+type rtm
 
-type message = (kam, Brg.term) Log.message
+type message = (rtm, Brg.term) Log.message
 
-val empty_kam: kam
+val empty_rtm: rtm
 
-val get: kam -> int -> Brg.bind
+val get: rtm -> int -> Brg.bind
 
-val push: kam -> Entity.node_attrs -> Brg.bind -> kam
+val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm
 
-val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term 
+val xwhd: Status.status -> rtm -> int option -> Brg.term -> rtm * Brg.term 
 
 (* arguments: expected type, inferred type *) 
 val are_convertible: 
-   Status.status -> kam -> int option -> Brg.term -> kam -> int option -> Brg.term -> bool
+   Status.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool
 
-val specs: (Level.status, kam, Brg.term) Log.specs
+val specs: (Level.status, rtm, Brg.term) Log.specs

diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli
index dd8e9a8f6462cbc29455eefea90749ab1eb1f5ef..f68259a6ec65e13bce92e3d17fe08d73f8d8d9f4 100644 (file)
--- 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.kam -> Brg.term -> 'a
+   Status.status -> BrgReduction.rtm -> Brg.term -> 'a

diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml
index 87a3f60cfff3942573016435c7466cc5597235f2..8425774d2a6bc890cb4cd439b67fec74ee9ab24c 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgUntrusted.ml
+++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml
@@ -27,7 +27,7 @@ let type_check err f st = function
       let f xt tt = 
          let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e
       in
-      BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_rtm t
    | ra, na, uri, E.Abbr t ->
       let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
@@ -37,7 +37,7 @@ let type_check err f st = function
         in
          let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
       in
-      BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_rtm t
    | _, _, _, E.Void       -> assert false
 
 let validate err f st e =
@@ -48,4 +48,4 @@ let validate err f st e =
    in
    let err msg = err (L.Uri uri :: msg) in
    let f () = let _ = BE.set_entity e in f () in
-   BV.validate err f st BR.empty_kam t
+   BV.validate err f st BR.empty_rtm t

diff --git a/helm/software/helena/src/basic_rg/brgValidity.mli b/helm/software/helena/src/basic_rg/brgValidity.mli
index 8ee88457d645b6d8088bd55bf78c6ebd5c2b542e..1b552b83c4e40848fcd7e6422dc92ecf3bdcd43f 100644 (file)
--- 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.kam -> Brg.term -> 'a
+   Status.status -> BrgReduction.rtm -> Brg.term -> 'a

diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml
index 51d6ddfc107df8323632f3f09a7abe9a389266f6..5fba63786ae75e42ce35175133a8150b22ca67e4 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -21,7 +21,7 @@ type reductions = {
    epsilon: int;
    ldelta : int;
    gdelta : int;
-   si     : int;
+   upsilon: int;
    lrt    : int;
    grt    : int;
    e      : int;
@@ -30,8 +30,8 @@ type reductions = {
 let level = 2
 
 let initial_reductions = {
-   beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0;
-   si = 0; lrt = 0; grt = 0; e = 0;
+   beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
+   lrt = 0; grt = 0; e = 0;
 }
 
 let reductions = ref initial_reductions
@@ -40,7 +40,7 @@ let clear_reductions () = reductions := initial_reductions
 
 let add 
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
-   ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
+   ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
 = reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
@@ -48,7 +48,7 @@ let add
    epsilon = !reductions.epsilon + epsilon;
    ldelta = !reductions.ldelta + ldelta;
    gdelta = !reductions.gdelta + gdelta;
-   si = !reductions.si + si;
+   upsilon = !reductions.upsilon + upsilon;
    lrt = !reductions.lrt + lrt;
    grt = !reductions.grt + grt;
    e = !reductions.e + e;
@@ -56,8 +56,8 @@ let add
 
 let print_reductions () =
    let r = !reductions in
-   let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in
-   let prs = r.si + r.lrt + r.grt + r.e in
+   let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in
+   let prs = r.lrt + r.grt + r.e in
    let delta = r.ldelta + r.gdelta in
    let rt = r.lrt + r.grt in
    L.warn level (P.sprintf "Reductions summary");
@@ -69,10 +69,10 @@ let print_reductions () =
    L.warn level (P.sprintf "    Theta:                  %7u" r.theta);
    L.warn level (P.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
    L.warn level (P.sprintf "    Zeta for cast:          %7u" r.epsilon);
+   L.warn level (P.sprintf "    Sort inclusion:         %7u" r.upsilon);
    L.warn level (P.sprintf "  Pseudo reductions:        %7u" prs);
    L.warn level (P.sprintf "    Reference typing:       %7u" rt);
    L.warn level (P.sprintf "      Local:                %7u" r.lrt);
    L.warn level (P.sprintf "      Global:               %7u" r.grt);
    L.warn level (P.sprintf "    Cast typing:            %7u" r.e);  
-   L.warn level (P.sprintf "    Sort inclusion:         %7u" r.si);
    L.warn level (P.sprintf "Relocated nodes (icm):      %7u" !G.icm)

diff --git a/helm/software/helena/src/common/output.mli b/helm/software/helena/src/common/output.mli
index ba2d294da73ca496c4604cdaeb076c35b7a945f0..3b6ecdab99d3d21c43920a0355627f6b073c342a 100644 (file)
--- a/helm/software/helena/src/common/output.mli
+++ b/helm/software/helena/src/common/output.mli
@@ -13,7 +13,7 @@ val clear_reductions: unit -> unit
 
 val add: 
    ?beta:int -> ?theta:int -> ?epsilon:int -> ?ldelta:int -> ?gdelta:int ->
-   ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> ?e:int ->
+   ?zeta:int -> ?upsilon:int -> ?lrt:int -> ?grt:int -> ?e:int ->
    unit -> unit
 
 val print_reductions: unit -> unit

diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml
index 89bf28e86e354dc3503c9c67cd16be77a41c87ba..401faf9aff450ec7936aba43b316661003a065d5 100644 (file)
--- a/helm/software/helena/src/common/status.ml
+++ b/helm/software/helena/src/common/status.ml
@@ -13,7 +13,6 @@ module G = Options
 module N = Level
 
 type status = {
-   delta: bool;    (* global delta-expansion *)
    si: bool;       (* sort inclusion *)
    lenv: N.status; (* level environment *)
 }
@@ -21,10 +20,9 @@ type status = {
 (* helpers ******************************************************************)
 
 let initial_status () = {
-   delta = false;
    si = !G.si; lenv = N.initial_status ();
 }
 
 let refresh_status st = {st with
-   si = !G.si; lenv = N.initial_status ();
+   si = !G.si (*; lenv = N.initial_status (); *)
 }