From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Sun, 29 Sep 2019 20:43:50 +0000 (+0200)
Subject: Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita... 
X-Git-Tag: make_still_working~229^2~1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=db020b4218272e2e35641ce3bc3b0a9b3afda899

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

db020b4218272e2e35641ce3bc3b0a9b3afda899
diff --cc matita/components/ng_tactics/.depend
index 90de5733d,4d386aaa4..57784f373
--- a/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 c8999df5a,ca420895d..75b2d57f8
--- a/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