Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita...

diff --cc matita/components/grafite/grafiteAstPp.ml
Simple merge

diff --cc matita/components/ng_tactics/.depend
index 90de5733d834f63c40b0c21c1b58de4b53f8d98e,4d386aaa4d37e5662f77a796b3acf2f9205b84f5..57784f373c6431d686960a318d050bad7555ac49
--- 1/matita/components/ng_tactics/.depend
--- 2/matita/components/ng_tactics/.depend
+++ b/matita/components/ng_tactics/.depend
@@@ -1,30 -1,94 +1,35 @@@
 -continuationals.cmo : \
 -    continuationals.cmi
 -continuationals.cmx : \
 -    continuationals.cmi
 +continuationals.cmo : continuationals.cmi
 +continuationals.cmx : continuationals.cmi
  continuationals.cmi :
 -declarative.cmo : \
 -    nnAuto.cmi \
 -    nTactics.cmi \
 -    nTacStatus.cmi \
 -    nCicElim.cmi \
 -    continuationals.cmi \
 -    declarative.cmi
 -declarative.cmx : \
 -    nnAuto.cmx \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    declarative.cmi
 -declarative.cmi : \
 -    nnAuto.cmi \
 -    nTacStatus.cmi
 -nCicElim.cmo : \
 -    nCicElim.cmi
 -nCicElim.cmx : \
 -    nCicElim.cmi
++declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi nCicElim.cmi \
++    continuationals.cmi declarative.cmi
++declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \
++    continuationals.cmx declarative.cmi
++declarative.cmi : nnAuto.cmi nTacStatus.cmi
 +nCicElim.cmo : nCicElim.cmi
 +nCicElim.cmx : nCicElim.cmi
  nCicElim.cmi :
 -nCicTacReduction.cmo : \
 -    nCicTacReduction.cmi
 -nCicTacReduction.cmx : \
 -    nCicTacReduction.cmi
 +nCicTacReduction.cmo : nCicTacReduction.cmi
 +nCicTacReduction.cmx : nCicTacReduction.cmi
  nCicTacReduction.cmi :
 -nDestructTac.cmo : \
 -    nTactics.cmi \
 -    nTacStatus.cmi \
 -    continuationals.cmi \
 +nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
      nDestructTac.cmi
 -nDestructTac.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    continuationals.cmx \
 +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
      nDestructTac.cmi
 -nDestructTac.cmi : \
 -    nTacStatus.cmi
 -nInversion.cmo : \
 -    nTactics.cmi \
 -    nTacStatus.cmi \
 -    nCicElim.cmi \
 -    continuationals.cmi \
 -    nInversion.cmi
 -nInversion.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    nInversion.cmi
 -nInversion.cmi : \
 -    nTacStatus.cmi
 -nTacStatus.cmo : \
 -    nCicTacReduction.cmi \
 -    continuationals.cmi \
 -    nTacStatus.cmi
 -nTacStatus.cmx : \
 -    nCicTacReduction.cmx \
 -    continuationals.cmx \
 -    nTacStatus.cmi
 -nTacStatus.cmi : \
 -    continuationals.cmi
 -nTactics.cmo : \
 -    nTacStatus.cmi \
 -    nCicElim.cmi \
 -    continuationals.cmi \
 -    nTactics.cmi
 -nTactics.cmx : \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    nTactics.cmi
 -nTactics.cmi : \
 -    nTacStatus.cmi
 -nnAuto.cmo : \
 -    nTactics.cmi \
 -    nTacStatus.cmi \
 -    nCicTacReduction.cmi \
 -    continuationals.cmi \
 -    nnAuto.cmi
 -nnAuto.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicTacReduction.cmx \
 -    continuationals.cmx \
 -    nnAuto.cmi
 -nnAuto.cmi : \
 -    nTacStatus.cmi
 +nDestructTac.cmi : nTacStatus.cmi
 +nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
 +    continuationals.cmi nInversion.cmi
 +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
 +    continuationals.cmx nInversion.cmi
 +nInversion.cmi : nTacStatus.cmi
 +nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
 +nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
 +nTacStatus.cmi : continuationals.cmi
 +nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
 +nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
 +nTactics.cmi : nTacStatus.cmi
 +nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
 +    continuationals.cmi nnAuto.cmi
 +nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
 +    continuationals.cmx nnAuto.cmi
 +nnAuto.cmi : nTacStatus.cmi

diff --cc matita/components/ng_tactics/.depend.opt
index c8999df5a2a69629233c9ad4d8ff3f228bd7f33f,ca420895d92c48c446b4bd70d62ac525f1353e7a..75b2d57f87f018d18706b67a4f16e67ea2b71b8c
--- 1/matita/components/ng_tactics/.depend.opt
--- 2/matita/components/ng_tactics/.depend.opt
+++ b/matita/components/ng_tactics/.depend.opt
@@@ -1,19 -1,55 +1,22 @@@
 -continuationals.cmx : \
 -    continuationals.cmi
 +continuationals.cmx : continuationals.cmi
  continuationals.cmi :
 -declarative.cmx : \
 -    nnAuto.cmx \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    declarative.cmi
 -declarative.cmi : \
 -    nnAuto.cmi \
 -    nTacStatus.cmi
 -nCicElim.cmx : \
 -    nCicElim.cmi
++declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \
++    continuationals.cmx declarative.cmi
++declarative.cmi : nnAuto.cmi nTacStatus.cmi
 +nCicElim.cmx : nCicElim.cmi
  nCicElim.cmi :
 -nCicTacReduction.cmx : \
 -    nCicTacReduction.cmi
 +nCicTacReduction.cmx : nCicTacReduction.cmi
  nCicTacReduction.cmi :
 -nDestructTac.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    continuationals.cmx \
 +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
      nDestructTac.cmi
 -nDestructTac.cmi : \
 -    nTacStatus.cmi
 -nInversion.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    nInversion.cmi
 -nInversion.cmi : \
 -    nTacStatus.cmi
 -nTacStatus.cmx : \
 -    nCicTacReduction.cmx \
 -    continuationals.cmx \
 -    nTacStatus.cmi
 -nTacStatus.cmi : \
 -    continuationals.cmi
 -nTactics.cmx : \
 -    nTacStatus.cmx \
 -    nCicElim.cmx \
 -    continuationals.cmx \
 -    nTactics.cmi
 -nTactics.cmi : \
 -    nTacStatus.cmi
 -nnAuto.cmx : \
 -    nTactics.cmx \
 -    nTacStatus.cmx \
 -    nCicTacReduction.cmx \
 -    continuationals.cmx \
 -    nnAuto.cmi
 -nnAuto.cmi : \
 -    nTacStatus.cmi
 +nDestructTac.cmi : nTacStatus.cmi
 +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
 +    continuationals.cmx nInversion.cmi
 +nInversion.cmi : nTacStatus.cmi
 +nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
 +nTacStatus.cmi : continuationals.cmi
 +nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
 +nTactics.cmi : nTacStatus.cmi
 +nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
 +    continuationals.cmx nnAuto.cmi
 +nnAuto.cmi : nTacStatus.cmi

diff --cc matita/components/ng_tactics/nTactics.ml
Simple merge