Dune sites used to locate the standard library

- it works both before and after installation
- it definitely breaks the Makefiles

diff --git a/matita/dune-project b/matita/dune-project
index 8a85936cced1b59e62387d8508c65eed26880068..67cf3618d8bf2255a942f359f550f56c7245ebaf 100644 (file)
--- a/matita/dune-project
+++ b/matita/dune-project
@@ -1,4 +1,5 @@
 (lang dune 3.6)
+(using dune_site 0.1)
 
 (name matita)
 
@@ -32,8 +33,10 @@
    (ocaml-expat (= 1.1.0))
    (lablgtk3-sourceview3 (= 3.1.3))
    dune-build-info
+   dune-site
    (camlp5 (= 8.00.04)))
  (tags
-  ("interactive theorem proving" "calculus of constructions")))
+  ("interactive theorem proving" "calculus of constructions"))
+ (sites (share myshare)))
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project

diff --git a/matita/matita.install b/matita/matita.install
index a90bb662d968ec8e0be05a127a78a21cac71e2bb..807e6514fd775f511e91a53137a6dd55dab3184e 100644 (file)
--- a/matita/matita.install
+++ b/matita/matita.install
@@ -8,375 +8,375 @@ bin: [
   "_build/install/default/bin/matitac"
   "_build/install/default/bin/matitaclean"
 ]
-share: [
-  "_build/install/default/share/matita/AUTHORS"
-  "_build/install/default/share/matita/LICENSE"
-  "_build/install/default/share/matita/closed.xml"
-  "_build/install/default/share/matita/help/C/Makefile" {"help/C/Makefile"}
-  "_build/install/default/share/matita/help/C/TODO" {"help/C/TODO"}
-  "_build/install/default/share/matita/help/C/declarative_tactics_quickref.xml" {"help/C/declarative_tactics_quickref.xml"}
-  "_build/install/default/share/matita/help/C/docbook.css" {"help/C/docbook.css"}
-  "_build/install/default/share/matita/help/C/figures/database.dia" {"help/C/figures/database.dia"}
-  "_build/install/default/share/matita/help/C/figures/database.png" {"help/C/figures/database.png"}
-  "_build/install/default/share/matita/help/C/figures/matita.png" {"help/C/figures/matita.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox1.png" {"help/C/figures/vbox1.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox2.png" {"help/C/figures/vbox2.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox3.png" {"help/C/figures/vbox3.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox35.png" {"help/C/figures/vbox35.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox4.png" {"help/C/figures/vbox4.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox5.png" {"help/C/figures/vbox5.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox6.png" {"help/C/figures/vbox6.png"}
-  "_build/install/default/share/matita/help/C/figures/vbox7.png" {"help/C/figures/vbox7.png"}
-  "_build/install/default/share/matita/help/C/legal.xml" {"help/C/legal.xml"}
-  "_build/install/default/share/matita/help/C/matita.xml" {"help/C/matita.xml"}
-  "_build/install/default/share/matita/help/C/scripts/fix-symbols.sh" {"help/C/scripts/fix-symbols.sh"}
-  "_build/install/default/share/matita/help/C/sec_commands.xml" {"help/C/sec_commands.xml"}
-  "_build/install/default/share/matita/help/C/sec_declarative_tactics.xml" {"help/C/sec_declarative_tactics.xml"}
-  "_build/install/default/share/matita/help/C/sec_gettingstarted.xml" {"help/C/sec_gettingstarted.xml"}
-  "_build/install/default/share/matita/help/C/sec_install.xml" {"help/C/sec_install.xml"}
-  "_build/install/default/share/matita/help/C/sec_intro.xml" {"help/C/sec_intro.xml"}
-  "_build/install/default/share/matita/help/C/sec_license.xml" {"help/C/sec_license.xml"}
-  "_build/install/default/share/matita/help/C/sec_tacticals.xml" {"help/C/sec_tacticals.xml"}
-  "_build/install/default/share/matita/help/C/sec_tactics.xml" {"help/C/sec_tactics.xml"}
-  "_build/install/default/share/matita/help/C/sec_terms.xml" {"help/C/sec_terms.xml"}
-  "_build/install/default/share/matita/help/C/sec_usernotation.xml" {"help/C/sec_usernotation.xml"}
-  "_build/install/default/share/matita/help/C/tactic_quickref.xml" {"help/C/tactic_quickref.xml"}
-  "_build/install/default/share/matita/help/C/tactics_quickref.xml" {"help/C/tactics_quickref.xml"}
-  "_build/install/default/share/matita/help/C/version.txt" {"help/C/version.txt"}
-  "_build/install/default/share/matita/help/C/version.txt.in" {"help/C/version.txt.in"}
-  "_build/install/default/share/matita/help/C/xhtml1-transitional.dtd" {"help/C/xhtml1-transitional.dtd"}
-  "_build/install/default/share/matita/help/C/xsl/matita-fo.xsl" {"help/C/xsl/matita-fo.xsl"}
-  "_build/install/default/share/matita/help/C/xsl/matita-xhtml.xsl" {"help/C/xsl/matita-xhtml.xsl"}
-  "_build/install/default/share/matita/help/C/xsl/tactic_quickref.xsl" {"help/C/xsl/tactic_quickref.xsl"}
-  "_build/install/default/share/matita/icons/matita-32.xpm" {"icons/matita-32.xpm"}
-  "_build/install/default/share/matita/icons/matita-bulb-high.png" {"icons/matita-bulb-high.png"}
-  "_build/install/default/share/matita/icons/matita-bulb-low.png" {"icons/matita-bulb-low.png"}
-  "_build/install/default/share/matita/icons/matita-bulb-medium.png" {"icons/matita-bulb-medium.png"}
-  "_build/install/default/share/matita/icons/matita-folder.png" {"icons/matita-folder.png"}
-  "_build/install/default/share/matita/icons/matita-object.png" {"icons/matita-object.png"}
-  "_build/install/default/share/matita/icons/matita-theory.png" {"icons/matita-theory.png"}
-  "_build/install/default/share/matita/icons/matita.png" {"icons/matita.png"}
-  "_build/install/default/share/matita/icons/matita_medium.png" {"icons/matita_medium.png"}
-  "_build/install/default/share/matita/icons/matita_small.png" {"icons/matita_small.png"}
-  "_build/install/default/share/matita/icons/matita_very_small.png" {"icons/matita_very_small.png"}
-  "_build/install/default/share/matita/icons/meegg.png" {"icons/meegg.png"}
-  "_build/install/default/share/matita/icons/whelp.png" {"icons/whelp.png"}
-  "_build/install/default/share/matita/icons/whelp.svg" {"icons/whelp.svg"}
-  "_build/install/default/share/matita/lib/MONADS/speranza.ma" {"lib/MONADS/speranza.ma"}
-  "_build/install/default/share/matita/lib/MONADS/speranza2.ma" {"lib/MONADS/speranza2.ma"}
-  "_build/install/default/share/matita/lib/Makefile" {"lib/Makefile"}
-  "_build/install/default/share/matita/lib/arithmetics/bigops.ma" {"lib/arithmetics/bigops.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/binomial.ma" {"lib/arithmetics/binomial.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/bounded_quantifiers.ma" {"lib/arithmetics/bounded_quantifiers.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/bertrand.ma" {"lib/arithmetics/chebyshev/bertrand.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/bertrand256.ma" {"lib/arithmetics/chebyshev/bertrand256.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma" {"lib/arithmetics/chebyshev/chebyshev_psi.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/chebyshev_theta.ma" {"lib/arithmetics/chebyshev/chebyshev_theta.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/factorization.ma" {"lib/arithmetics/chebyshev/factorization.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chebyshev/psi_bounds.ma" {"lib/arithmetics/chebyshev/psi_bounds.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/chinese_reminder.ma" {"lib/arithmetics/chinese_reminder.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/congruence.ma" {"lib/arithmetics/congruence.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/div_and_mod.ma" {"lib/arithmetics/div_and_mod.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/exp.ma" {"lib/arithmetics/exp.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/factorial.ma" {"lib/arithmetics/factorial.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/fermat_little_theorem.ma" {"lib/arithmetics/fermat_little_theorem.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/gcd.ma" {"lib/arithmetics/gcd.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/iteration.ma" {"lib/arithmetics/iteration.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/log.ma" {"lib/arithmetics/log.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/lstar.ma" {"lib/arithmetics/lstar.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/minimization.ma" {"lib/arithmetics/minimization.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/nat.ma" {"lib/arithmetics/nat.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/nat_commented.ma" {"lib/arithmetics/nat_commented.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/nth_prime.ma" {"lib/arithmetics/nth_prime.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/ord.ma" {"lib/arithmetics/ord.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/permutation.ma" {"lib/arithmetics/permutation.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/pidgeon_hole.ma" {"lib/arithmetics/pidgeon_hole.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/primes.ma" {"lib/arithmetics/primes.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/sigma_pi.ma" {"lib/arithmetics/sigma_pi.ma"}
-  "_build/install/default/share/matita/lib/arithmetics/sqrt.ma" {"lib/arithmetics/sqrt.ma"}
-  "_build/install/default/share/matita/lib/basics/bool.ma" {"lib/basics/bool.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation.ma" {"lib/basics/core_notation.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/apart_2.ma" {"lib/basics/core_notation/apart_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/card_1.ma" {"lib/basics/core_notation/card_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/compose_2.ma" {"lib/basics/core_notation/compose_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/comprehension_2.ma" {"lib/basics/core_notation/comprehension_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/downarrow_1.ma" {"lib/basics/core_notation/downarrow_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/exp_2.ma" {"lib/basics/core_notation/exp_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/fact_1.ma" {"lib/basics/core_notation/fact_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/fintersects_2.ma" {"lib/basics/core_notation/fintersects_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/funion_2.ma" {"lib/basics/core_notation/funion_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/invert_1.ma" {"lib/basics/core_notation/invert_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/invert_appl_2.ma" {"lib/basics/core_notation/invert_appl_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/napart_2.ma" {"lib/basics/core_notation/napart_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/overlaps_2.ma" {"lib/basics/core_notation/overlaps_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/pair_2.ma" {"lib/basics/core_notation/pair_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/singl_1.ma" {"lib/basics/core_notation/singl_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/subset_1.ma" {"lib/basics/core_notation/subset_1.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/subseteq_2.ma" {"lib/basics/core_notation/subseteq_2.ma"}
-  "_build/install/default/share/matita/lib/basics/core_notation/uparrow_1.ma" {"lib/basics/core_notation/uparrow_1.ma"}
-  "_build/install/default/share/matita/lib/basics/deqlist.ma" {"lib/basics/deqlist.ma"}
-  "_build/install/default/share/matita/lib/basics/deqsets.ma" {"lib/basics/deqsets.ma"}
-  "_build/install/default/share/matita/lib/basics/finset.ma" {"lib/basics/finset.ma"}
-  "_build/install/default/share/matita/lib/basics/jmeq.ma" {"lib/basics/jmeq.ma"}
-  "_build/install/default/share/matita/lib/basics/lists/list.ma" {"lib/basics/lists/list.ma"}
-  "_build/install/default/share/matita/lib/basics/lists/listb.ma" {"lib/basics/lists/listb.ma"}
-  "_build/install/default/share/matita/lib/basics/lists/lstar.ma" {"lib/basics/lists/lstar.ma"}
-  "_build/install/default/share/matita/lib/basics/logic.ma" {"lib/basics/logic.ma"}
-  "_build/install/default/share/matita/lib/basics/pts.ma" {"lib/basics/pts.ma"}
-  "_build/install/default/share/matita/lib/basics/relations.ma" {"lib/basics/relations.ma"}
-  "_build/install/default/share/matita/lib/basics/russell.ma" {"lib/basics/russell.ma"}
-  "_build/install/default/share/matita/lib/basics/sets.ma" {"lib/basics/sets.ma"}
-  "_build/install/default/share/matita/lib/basics/star.ma" {"lib/basics/star.ma"}
-  "_build/install/default/share/matita/lib/basics/star1.ma" {"lib/basics/star1.ma"}
-  "_build/install/default/share/matita/lib/basics/types.ma" {"lib/basics/types.ma"}
-  "_build/install/default/share/matita/lib/basics/vector_finset.ma" {"lib/basics/vector_finset.ma"}
-  "_build/install/default/share/matita/lib/basics/vectors.ma" {"lib/basics/vectors.ma"}
-  "_build/install/default/share/matita/lib/didactic/natural_deduction.ma" {"lib/didactic/natural_deduction.ma"}
-  "_build/install/default/share/matita/lib/extraction.ma" {"lib/extraction.ma"}
-  "_build/install/default/share/matita/lib/fail.txt" {"lib/fail.txt"}
-  "_build/install/default/share/matita/lib/finite_lambda/confluence.ma" {"lib/finite_lambda/confluence.ma"}
-  "_build/install/default/share/matita/lib/finite_lambda/reduction.ma" {"lib/finite_lambda/reduction.ma"}
-  "_build/install/default/share/matita/lib/finite_lambda/terms_and_types.ma" {"lib/finite_lambda/terms_and_types.ma"}
-  "_build/install/default/share/matita/lib/finite_lambda/typing.ma" {"lib/finite_lambda/typing.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/apply_functor.ma" {"lib/formal_topology/apply_functor.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/basic_pairs.ma" {"lib/formal_topology/basic_pairs.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma" {"lib/formal_topology/basic_pairs_to_basic_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma" {"lib/formal_topology/basic_pairs_to_o-basic_pairs.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/basic_topologies.ma" {"lib/formal_topology/basic_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma" {"lib/formal_topology/basic_topologies_to_o-basic_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/categories.ma" {"lib/formal_topology/categories.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/concrete_spaces.ma" {"lib/formal_topology/concrete_spaces.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma" {"lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/cprop_connectives.ma" {"lib/formal_topology/cprop_connectives.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/formal_topologies.ma" {"lib/formal_topology/formal_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/notation.ma" {"lib/formal_topology/notation.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-algebra.ma" {"lib/formal_topology/o-algebra.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-basic_pairs.ma" {"lib/formal_topology/o-basic_pairs.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma" {"lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-basic_topologies.ma" {"lib/formal_topology/o-basic_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-concrete_spaces.ma" {"lib/formal_topology/o-concrete_spaces.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-formal_topologies.ma" {"lib/formal_topology/o-formal_topologies.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/o-saturations.ma" {"lib/formal_topology/o-saturations.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/r-o-basic_pairs.ma" {"lib/formal_topology/r-o-basic_pairs.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/relations.ma" {"lib/formal_topology/relations.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/relations_to_o-algebra.ma" {"lib/formal_topology/relations_to_o-algebra.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/replace.sh" {"lib/formal_topology/replace.sh"}
-  "_build/install/default/share/matita/lib/formal_topology/saturations.ma" {"lib/formal_topology/saturations.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/saturations_to_o-saturations.ma" {"lib/formal_topology/saturations_to_o-saturations.ma"}
-  "_build/install/default/share/matita/lib/formal_topology/subsets.ma" {"lib/formal_topology/subsets.ma"}
-  "_build/install/default/share/matita/lib/hints_declaration.ma" {"lib/hints_declaration.ma"}
-  "_build/install/default/share/matita/lib/hott/Overture.ma" {"lib/hott/Overture.ma"}
-  "_build/install/default/share/matita/lib/hott/PathGroupoids.ma" {"lib/hott/PathGroupoids.ma"}
-  "_build/install/default/share/matita/lib/hott/notations.ma" {"lib/hott/notations.ma"}
-  "_build/install/default/share/matita/lib/hott/pts.ma" {"lib/hott/pts.ma"}
-  "_build/install/default/share/matita/lib/hott/types.ma" {"lib/hott/types.ma"}
-  "_build/install/default/share/matita/lib/inconsistent.ma" {"lib/inconsistent.ma"}
-  "_build/install/default/share/matita/lib/lambda/Makefile" {"lib/lambda/Makefile"}
-  "_build/install/default/share/matita/lib/lambda/background/preamble.ma" {"lib/lambda/background/preamble.ma"}
-  "_build/install/default/share/matita/lib/lambda/etc/cons_r.etc" {"lib/lambda/etc/cons_r.etc"}
-  "_build/install/default/share/matita/lib/lambda/levels/interpretations.ma" {"lib/lambda/levels/interpretations.ma"}
-  "_build/install/default/share/matita/lib/lambda/levels/iterated_abstraction.ma" {"lib/lambda/levels/iterated_abstraction.ma"}
-  "_build/install/default/share/matita/lib/lambda/levels/term.ma" {"lib/lambda/levels/term.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/abstraction_1.ma" {"lib/lambda/notation/functions/abstraction_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/abstraction_2.ma" {"lib/lambda/notation/functions/abstraction_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/annotatedabstraction_2.ma" {"lib/lambda/notation/functions/annotatedabstraction_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/application_2.ma" {"lib/lambda/notation/functions/application_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/application_3.ma" {"lib/lambda/notation/functions/application_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/backward_1.ma" {"lib/lambda/notation/functions/backward_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/backward_3.ma" {"lib/lambda/notation/functions/backward_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/dsubst_3.ma" {"lib/lambda/notation/functions/dsubst_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/forward_1.ma" {"lib/lambda/notation/functions/forward_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/forward_3.ma" {"lib/lambda/notation/functions/forward_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/hocons_2.ma" {"lib/lambda/notation/functions/hocons_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/lift_3.ma" {"lib/lambda/notation/functions/lift_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/multiplicity_1.ma" {"lib/lambda/notation/functions/multiplicity_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/nil_0.ma" {"lib/lambda/notation/functions/nil_0.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/projectdown_1.ma" {"lib/lambda/notation/functions/projectdown_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/projectsame_2.ma" {"lib/lambda/notation/functions/projectsame_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/projectup_2.ma" {"lib/lambda/notation/functions/projectup_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/variablereferencebyindex_1.ma" {"lib/lambda/notation/functions/variablereferencebyindex_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/variablereferencebyindex_2.ma" {"lib/lambda/notation/functions/variablereferencebyindex_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/functions/variablereferencebylevel_2.ma" {"lib/lambda/notation/functions/variablereferencebylevel_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/decomposedstd_2.ma" {"lib/lambda/notation/relations/decomposedstd_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/parred_2.ma" {"lib/lambda/notation/relations/parred_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/parredstar_2.ma" {"lib/lambda/notation/relations/parredstar_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/prec_2.ma" {"lib/lambda/notation/relations/prec_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/seqred_2.ma" {"lib/lambda/notation/relations/seqred_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/seqred_3.ma" {"lib/lambda/notation/relations/seqred_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/seqredstar_2.ma" {"lib/lambda/notation/relations/seqredstar_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/seqredstar_3.ma" {"lib/lambda/notation/relations/seqredstar_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/std_3.ma" {"lib/lambda/notation/relations/std_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/relations/stdstar_3.ma" {"lib/lambda/notation/relations/stdstar_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_1_2.ma" {"lib/lambda/notation/xoa/ex_1_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_2_2.ma" {"lib/lambda/notation/xoa/ex_2_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_2_3.ma" {"lib/lambda/notation/xoa/ex_2_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_3_1.ma" {"lib/lambda/notation/xoa/ex_3_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_3_2.ma" {"lib/lambda/notation/xoa/ex_3_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_3_3.ma" {"lib/lambda/notation/xoa/ex_3_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_3_4.ma" {"lib/lambda/notation/xoa/ex_3_4.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_4_1.ma" {"lib/lambda/notation/xoa/ex_4_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_4_2.ma" {"lib/lambda/notation/xoa/ex_4_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/ex_4_3.ma" {"lib/lambda/notation/xoa/ex_4_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/false_0.ma" {"lib/lambda/notation/xoa/false_0.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/or_3.ma" {"lib/lambda/notation/xoa/or_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/notation/xoa/true_0.ma" {"lib/lambda/notation/xoa/true_0.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/alternative_standard_order.ma" {"lib/lambda/paths/alternative_standard_order.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/decomposed_trace.ma" {"lib/lambda/paths/decomposed_trace.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/dst_computation.ma" {"lib/lambda/paths/dst_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/labeled_sequential_computation.ma" {"lib/lambda/paths/labeled_sequential_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/labeled_sequential_reduction.ma" {"lib/lambda/paths/labeled_sequential_reduction.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/labeled_st_computation.ma" {"lib/lambda/paths/labeled_st_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/labeled_st_reduction.ma" {"lib/lambda/paths/labeled_st_reduction.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/path.ma" {"lib/lambda/paths/path.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/standard_order.ma" {"lib/lambda/paths/standard_order.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/standard_precedence.ma" {"lib/lambda/paths/standard_precedence.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/standard_trace.ma" {"lib/lambda/paths/standard_trace.ma"}
-  "_build/install/default/share/matita/lib/lambda/paths/trace.ma" {"lib/lambda/paths/trace.ma"}
-  "_build/install/default/share/matita/lib/lambda/policy.txt" {"lib/lambda/policy.txt"}
-  "_build/install/default/share/matita/lib/lambda/replace.sh" {"lib/lambda/replace.sh"}
-  "_build/install/default/share/matita/lib/lambda/subterms/boolean.ma" {"lib/lambda/subterms/boolean.ma"}
-  "_build/install/default/share/matita/lib/lambda/subterms/booleanized.ma" {"lib/lambda/subterms/booleanized.ma"}
-  "_build/install/default/share/matita/lib/lambda/subterms/carrier.ma" {"lib/lambda/subterms/carrier.ma"}
-  "_build/install/default/share/matita/lib/lambda/subterms/relocating_substitution.ma" {"lib/lambda/subterms/relocating_substitution.ma"}
-  "_build/install/default/share/matita/lib/lambda/subterms/relocation.ma" {"lib/lambda/subterms/relocation.ma"}
-  "_build/install/default/share/matita/lib/lambda/subterms/subterms.ma" {"lib/lambda/subterms/subterms.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/iterated_abstraction.ma" {"lib/lambda/terms/iterated_abstraction.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/labeled_sequential_computation.ma" {"lib/lambda/terms/labeled_sequential_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/multiplicity.ma" {"lib/lambda/terms/multiplicity.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/parallel_computation.ma" {"lib/lambda/terms/parallel_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/parallel_reduction.ma" {"lib/lambda/terms/parallel_reduction.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/relocating_substitution.ma" {"lib/lambda/terms/relocating_substitution.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/relocation.ma" {"lib/lambda/terms/relocation.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/sequential_computation.ma" {"lib/lambda/terms/sequential_computation.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/sequential_reduction.ma" {"lib/lambda/terms/sequential_reduction.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/size.ma" {"lib/lambda/terms/size.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/supercombinator.ma" {"lib/lambda/terms/supercombinator.ma"}
-  "_build/install/default/share/matita/lib/lambda/terms/term.ma" {"lib/lambda/terms/term.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa.conf.xml" {"lib/lambda/xoa.conf.xml"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_1_2.ma" {"lib/lambda/xoa/ex_1_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_2_2.ma" {"lib/lambda/xoa/ex_2_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_2_3.ma" {"lib/lambda/xoa/ex_2_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_3_1.ma" {"lib/lambda/xoa/ex_3_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_3_2.ma" {"lib/lambda/xoa/ex_3_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_3_3.ma" {"lib/lambda/xoa/ex_3_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_3_4.ma" {"lib/lambda/xoa/ex_3_4.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_4_1.ma" {"lib/lambda/xoa/ex_4_1.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_4_2.ma" {"lib/lambda/xoa/ex_4_2.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/ex_4_3.ma" {"lib/lambda/xoa/ex_4_3.ma"}
-  "_build/install/default/share/matita/lib/lambda/xoa/or_3.ma" {"lib/lambda/xoa/or_3.ma"}
-  "_build/install/default/share/matita/lib/preamble.hs" {"lib/preamble.hs"}
-  "_build/install/default/share/matita/lib/preamble.ml" {"lib/preamble.ml"}
-  "_build/install/default/share/matita/lib/pts_dummy/CC2FO_K.ma" {"lib/pts_dummy/CC2FO_K.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/CC2FO_K_cube.ma" {"lib/pts_dummy/CC2FO_K_cube.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/arity.ma" {"lib/pts_dummy/arity.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/arity_eval.ma" {"lib/pts_dummy/arity_eval.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/convertibility.ma" {"lib/pts_dummy/convertibility.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/cube.ma" {"lib/pts_dummy/cube.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/degree.ma" {"lib/pts_dummy/degree.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/ext.ma" {"lib/pts_dummy/ext.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/ext_lambda.ma" {"lib/pts_dummy/ext_lambda.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/inversion.ma" {"lib/pts_dummy/inversion.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/lambda_notation.ma" {"lib/pts_dummy/lambda_notation.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/lift.ma" {"lib/pts_dummy/lift.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/par_reduction.ma" {"lib/pts_dummy/par_reduction.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/rc_eval.ma" {"lib/pts_dummy/rc_eval.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/rc_hsat.ma" {"lib/pts_dummy/rc_hsat.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/rc_sat.ma" {"lib/pts_dummy/rc_sat.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/reduction.ma" {"lib/pts_dummy/reduction.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/sn.ma" {"lib/pts_dummy/sn.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/subject.ma" {"lib/pts_dummy/subject.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/subst.ma" {"lib/pts_dummy/subst.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/subterms.ma" {"lib/pts_dummy/subterms.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/terms.ma" {"lib/pts_dummy/terms.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy/types.ma" {"lib/pts_dummy/types.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/arity.ma" {"lib/pts_dummy_new/arity.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/arity_eval.ma" {"lib/pts_dummy_new/arity_eval.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/convertibility.ma" {"lib/pts_dummy_new/convertibility.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/cube.ma" {"lib/pts_dummy_new/cube.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/ext.ma" {"lib/pts_dummy_new/ext.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/ext_lambda.ma" {"lib/pts_dummy_new/ext_lambda.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/inversion.ma" {"lib/pts_dummy_new/inversion.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/lambda_notation.ma" {"lib/pts_dummy_new/lambda_notation.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/par_reduction.ma" {"lib/pts_dummy_new/par_reduction.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/rc_eval.ma" {"lib/pts_dummy_new/rc_eval.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/rc_hsat.ma" {"lib/pts_dummy_new/rc_hsat.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/rc_sat.ma" {"lib/pts_dummy_new/rc_sat.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/reduction.ma" {"lib/pts_dummy_new/reduction.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/sn.ma" {"lib/pts_dummy_new/sn.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/subject.ma" {"lib/pts_dummy_new/subject.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/subst.ma" {"lib/pts_dummy_new/subst.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/subterms.ma" {"lib/pts_dummy_new/subterms.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/terms.ma" {"lib/pts_dummy_new/terms.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/thinning.ma" {"lib/pts_dummy_new/thinning.ma"}
-  "_build/install/default/share/matita/lib/pts_dummy_new/types.ma" {"lib/pts_dummy_new/types.ma"}
-  "_build/install/default/share/matita/lib/re/lang.ma" {"lib/re/lang.ma"}
-  "_build/install/default/share/matita/lib/re/moves.ma" {"lib/re/moves.ma"}
-  "_build/install/default/share/matita/lib/re/re.ma" {"lib/re/re.ma"}
-  "_build/install/default/share/matita/lib/re/reb.ma" {"lib/re/reb.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/almost.ma" {"lib/reverse_complexity/almost.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/basics.ma" {"lib/reverse_complexity/basics.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/big_O.ma" {"lib/reverse_complexity/big_O.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/bigops_compl.ma" {"lib/reverse_complexity/bigops_compl.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/complexity.ma" {"lib/reverse_complexity/complexity.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/gap.ma" {"lib/reverse_complexity/gap.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/hierarchy.ma" {"lib/reverse_complexity/hierarchy.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/sigma_diseq.ma" {"lib/reverse_complexity/sigma_diseq.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/speed_clean.ma" {"lib/reverse_complexity/speed_clean.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/speed_def.ma" {"lib/reverse_complexity/speed_def.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/speed_new.ma" {"lib/reverse_complexity/speed_new.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/speedup.ma" {"lib/reverse_complexity/speedup.ma"}
-  "_build/install/default/share/matita/lib/reverse_complexity/toolkit.ma" {"lib/reverse_complexity/toolkit.ma"}
-  "_build/install/default/share/matita/lib/root" {"lib/root"}
-  "_build/install/default/share/matita/lib/self_typing.ma" {"lib/self_typing.ma"}
-  "_build/install/default/share/matita/lib/turing/auxiliary_machines.ma" {"lib/turing/auxiliary_machines.ma"}
-  "_build/install/default/share/matita/lib/turing/auxiliary_machines1.ma" {"lib/turing/auxiliary_machines1.ma"}
-  "_build/install/default/share/matita/lib/turing/auxiliary_multi_machines.ma" {"lib/turing/auxiliary_multi_machines.ma"}
-  "_build/install/default/share/matita/lib/turing/basic_machines.ma" {"lib/turing/basic_machines.ma"}
-  "_build/install/default/share/matita/lib/turing/basic_multi_machines.ma" {"lib/turing/basic_multi_machines.ma"}
-  "_build/install/default/share/matita/lib/turing/complexity.ma" {"lib/turing/complexity.ma"}
-  "_build/install/default/share/matita/lib/turing/if_machine.ma" {"lib/turing/if_machine.ma"}
-  "_build/install/default/share/matita/lib/turing/if_multi.ma" {"lib/turing/if_multi.ma"}
-  "_build/install/default/share/matita/lib/turing/inject.ma" {"lib/turing/inject.ma"}
-  "_build/install/default/share/matita/lib/turing/mono.ma" {"lib/turing/mono.ma"}
-  "_build/install/default/share/matita/lib/turing/move_char.ma" {"lib/turing/move_char.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/exec_moves.ma" {"lib/turing/multi_to_mono/exec_moves.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/exec_trace_move.ma" {"lib/turing/multi_to_mono/exec_trace_move.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/full.ma" {"lib/turing/multi_to_mono/full.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/shift_trace.ma" {"lib/turing/multi_to_mono/shift_trace.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/shift_trace_aux.ma" {"lib/turing/multi_to_mono/shift_trace_aux.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/step.ma" {"lib/turing/multi_to_mono/step.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_to_mono/trace_alphabet.ma" {"lib/turing/multi_to_mono/trace_alphabet.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/alphabet.ma" {"lib/turing/multi_universal/alphabet.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/binaryTM.ma" {"lib/turing/multi_universal/binaryTM.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/match.ma" {"lib/turing/multi_universal/match.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/normalTM.ma" {"lib/turing/multi_universal/normalTM.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/tuples.ma" {"lib/turing/multi_universal/tuples.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/unistep.ma" {"lib/turing/multi_universal/unistep.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/unistep_aux.ma" {"lib/turing/multi_universal/unistep_aux.ma"}
-  "_build/install/default/share/matita/lib/turing/multi_universal/universal.ma" {"lib/turing/multi_universal/universal.ma"}
-  "_build/install/default/share/matita/lib/turing/ntm.ma" {"lib/turing/ntm.ma"}
-  "_build/install/default/share/matita/lib/turing/oracle.ma" {"lib/turing/oracle.ma"}
-  "_build/install/default/share/matita/lib/turing/turing.ma" {"lib/turing/turing.ma"}
-  "_build/install/default/share/matita/lib/turing/turing_old.ma" {"lib/turing/turing_old.ma"}
-  "_build/install/default/share/matita/lib/turing/universal.ma" {"lib/turing/universal.ma"}
-  "_build/install/default/share/matita/lib/turing/while_machine.ma" {"lib/turing/while_machine.ma"}
-  "_build/install/default/share/matita/lib/turing/while_multi.ma" {"lib/turing/while_multi.ma"}
-  "_build/install/default/share/matita/lib/turing/wmono.ma" {"lib/turing/wmono.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter1.ma" {"lib/tutorial/chapter1.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter10.ma" {"lib/tutorial/chapter10.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter11.ma" {"lib/tutorial/chapter11.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter12.ma" {"lib/tutorial/chapter12.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter13.ma" {"lib/tutorial/chapter13.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter2.ma" {"lib/tutorial/chapter2.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter3.ma" {"lib/tutorial/chapter3.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter4.ma" {"lib/tutorial/chapter4.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter5.ma" {"lib/tutorial/chapter5.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter6.ma" {"lib/tutorial/chapter6.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter7.ma" {"lib/tutorial/chapter7.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter8.ma" {"lib/tutorial/chapter8.ma"}
-  "_build/install/default/share/matita/lib/tutorial/chapter9.ma" {"lib/tutorial/chapter9.ma"}
-  "_build/install/default/share/matita/matita.conf.xml"
-  "_build/install/default/share/matita/matita.gtkrc"
-  "_build/install/default/share/matita/matita.lang"
-  "_build/install/default/share/matita/matita.ma.templ"
+share_root: [
+  "_build/install/default/share/matita/myshare/AUTHORS" {"matita/myshare/AUTHORS"}
+  "_build/install/default/share/matita/myshare/LICENSE" {"matita/myshare/LICENSE"}
+  "_build/install/default/share/matita/myshare/closed.xml" {"matita/myshare/closed.xml"}
+  "_build/install/default/share/matita/myshare/help/C/Makefile" {"matita/myshare/help/C/Makefile"}
+  "_build/install/default/share/matita/myshare/help/C/TODO" {"matita/myshare/help/C/TODO"}
+  "_build/install/default/share/matita/myshare/help/C/declarative_tactics_quickref.xml" {"matita/myshare/help/C/declarative_tactics_quickref.xml"}
+  "_build/install/default/share/matita/myshare/help/C/docbook.css" {"matita/myshare/help/C/docbook.css"}
+  "_build/install/default/share/matita/myshare/help/C/figures/database.dia" {"matita/myshare/help/C/figures/database.dia"}
+  "_build/install/default/share/matita/myshare/help/C/figures/database.png" {"matita/myshare/help/C/figures/database.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/matita.png" {"matita/myshare/help/C/figures/matita.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox1.png" {"matita/myshare/help/C/figures/vbox1.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox2.png" {"matita/myshare/help/C/figures/vbox2.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox3.png" {"matita/myshare/help/C/figures/vbox3.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox35.png" {"matita/myshare/help/C/figures/vbox35.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox4.png" {"matita/myshare/help/C/figures/vbox4.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox5.png" {"matita/myshare/help/C/figures/vbox5.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox6.png" {"matita/myshare/help/C/figures/vbox6.png"}
+  "_build/install/default/share/matita/myshare/help/C/figures/vbox7.png" {"matita/myshare/help/C/figures/vbox7.png"}
+  "_build/install/default/share/matita/myshare/help/C/legal.xml" {"matita/myshare/help/C/legal.xml"}
+  "_build/install/default/share/matita/myshare/help/C/matita.xml" {"matita/myshare/help/C/matita.xml"}
+  "_build/install/default/share/matita/myshare/help/C/scripts/fix-symbols.sh" {"matita/myshare/help/C/scripts/fix-symbols.sh"}
+  "_build/install/default/share/matita/myshare/help/C/sec_commands.xml" {"matita/myshare/help/C/sec_commands.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_declarative_tactics.xml" {"matita/myshare/help/C/sec_declarative_tactics.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_gettingstarted.xml" {"matita/myshare/help/C/sec_gettingstarted.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_install.xml" {"matita/myshare/help/C/sec_install.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_intro.xml" {"matita/myshare/help/C/sec_intro.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_license.xml" {"matita/myshare/help/C/sec_license.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_tacticals.xml" {"matita/myshare/help/C/sec_tacticals.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_tactics.xml" {"matita/myshare/help/C/sec_tactics.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_terms.xml" {"matita/myshare/help/C/sec_terms.xml"}
+  "_build/install/default/share/matita/myshare/help/C/sec_usernotation.xml" {"matita/myshare/help/C/sec_usernotation.xml"}
+  "_build/install/default/share/matita/myshare/help/C/tactic_quickref.xml" {"matita/myshare/help/C/tactic_quickref.xml"}
+  "_build/install/default/share/matita/myshare/help/C/tactics_quickref.xml" {"matita/myshare/help/C/tactics_quickref.xml"}
+  "_build/install/default/share/matita/myshare/help/C/version.txt" {"matita/myshare/help/C/version.txt"}
+  "_build/install/default/share/matita/myshare/help/C/version.txt.in" {"matita/myshare/help/C/version.txt.in"}
+  "_build/install/default/share/matita/myshare/help/C/xhtml1-transitional.dtd" {"matita/myshare/help/C/xhtml1-transitional.dtd"}
+  "_build/install/default/share/matita/myshare/help/C/xsl/matita-fo.xsl" {"matita/myshare/help/C/xsl/matita-fo.xsl"}
+  "_build/install/default/share/matita/myshare/help/C/xsl/matita-xhtml.xsl" {"matita/myshare/help/C/xsl/matita-xhtml.xsl"}
+  "_build/install/default/share/matita/myshare/help/C/xsl/tactic_quickref.xsl" {"matita/myshare/help/C/xsl/tactic_quickref.xsl"}
+  "_build/install/default/share/matita/myshare/icons/matita-32.xpm" {"matita/myshare/icons/matita-32.xpm"}
+  "_build/install/default/share/matita/myshare/icons/matita-bulb-high.png" {"matita/myshare/icons/matita-bulb-high.png"}
+  "_build/install/default/share/matita/myshare/icons/matita-bulb-low.png" {"matita/myshare/icons/matita-bulb-low.png"}
+  "_build/install/default/share/matita/myshare/icons/matita-bulb-medium.png" {"matita/myshare/icons/matita-bulb-medium.png"}
+  "_build/install/default/share/matita/myshare/icons/matita-folder.png" {"matita/myshare/icons/matita-folder.png"}
+  "_build/install/default/share/matita/myshare/icons/matita-object.png" {"matita/myshare/icons/matita-object.png"}
+  "_build/install/default/share/matita/myshare/icons/matita-theory.png" {"matita/myshare/icons/matita-theory.png"}
+  "_build/install/default/share/matita/myshare/icons/matita.png" {"matita/myshare/icons/matita.png"}
+  "_build/install/default/share/matita/myshare/icons/matita_medium.png" {"matita/myshare/icons/matita_medium.png"}
+  "_build/install/default/share/matita/myshare/icons/matita_small.png" {"matita/myshare/icons/matita_small.png"}
+  "_build/install/default/share/matita/myshare/icons/matita_very_small.png" {"matita/myshare/icons/matita_very_small.png"}
+  "_build/install/default/share/matita/myshare/icons/meegg.png" {"matita/myshare/icons/meegg.png"}
+  "_build/install/default/share/matita/myshare/icons/whelp.png" {"matita/myshare/icons/whelp.png"}
+  "_build/install/default/share/matita/myshare/icons/whelp.svg" {"matita/myshare/icons/whelp.svg"}
+  "_build/install/default/share/matita/myshare/lib/MONADS/speranza.ma" {"matita/myshare/lib/MONADS/speranza.ma"}
+  "_build/install/default/share/matita/myshare/lib/MONADS/speranza2.ma" {"matita/myshare/lib/MONADS/speranza2.ma"}
+  "_build/install/default/share/matita/myshare/lib/Makefile" {"matita/myshare/lib/Makefile"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/bigops.ma" {"matita/myshare/lib/arithmetics/bigops.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/binomial.ma" {"matita/myshare/lib/arithmetics/binomial.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/bounded_quantifiers.ma" {"matita/myshare/lib/arithmetics/bounded_quantifiers.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/bertrand.ma" {"matita/myshare/lib/arithmetics/chebyshev/bertrand.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/bertrand256.ma" {"matita/myshare/lib/arithmetics/chebyshev/bertrand256.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/chebyshev_psi.ma" {"matita/myshare/lib/arithmetics/chebyshev/chebyshev_psi.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/chebyshev_theta.ma" {"matita/myshare/lib/arithmetics/chebyshev/chebyshev_theta.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/factorization.ma" {"matita/myshare/lib/arithmetics/chebyshev/factorization.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chebyshev/psi_bounds.ma" {"matita/myshare/lib/arithmetics/chebyshev/psi_bounds.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/chinese_reminder.ma" {"matita/myshare/lib/arithmetics/chinese_reminder.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/congruence.ma" {"matita/myshare/lib/arithmetics/congruence.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/div_and_mod.ma" {"matita/myshare/lib/arithmetics/div_and_mod.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/exp.ma" {"matita/myshare/lib/arithmetics/exp.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/factorial.ma" {"matita/myshare/lib/arithmetics/factorial.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/fermat_little_theorem.ma" {"matita/myshare/lib/arithmetics/fermat_little_theorem.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/gcd.ma" {"matita/myshare/lib/arithmetics/gcd.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/iteration.ma" {"matita/myshare/lib/arithmetics/iteration.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/log.ma" {"matita/myshare/lib/arithmetics/log.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/lstar.ma" {"matita/myshare/lib/arithmetics/lstar.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/minimization.ma" {"matita/myshare/lib/arithmetics/minimization.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/nat.ma" {"matita/myshare/lib/arithmetics/nat.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/nat_commented.ma" {"matita/myshare/lib/arithmetics/nat_commented.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/nth_prime.ma" {"matita/myshare/lib/arithmetics/nth_prime.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/ord.ma" {"matita/myshare/lib/arithmetics/ord.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/permutation.ma" {"matita/myshare/lib/arithmetics/permutation.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/pidgeon_hole.ma" {"matita/myshare/lib/arithmetics/pidgeon_hole.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/primes.ma" {"matita/myshare/lib/arithmetics/primes.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/sigma_pi.ma" {"matita/myshare/lib/arithmetics/sigma_pi.ma"}
+  "_build/install/default/share/matita/myshare/lib/arithmetics/sqrt.ma" {"matita/myshare/lib/arithmetics/sqrt.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/bool.ma" {"matita/myshare/lib/basics/bool.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation.ma" {"matita/myshare/lib/basics/core_notation.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/apart_2.ma" {"matita/myshare/lib/basics/core_notation/apart_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/card_1.ma" {"matita/myshare/lib/basics/core_notation/card_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/compose_2.ma" {"matita/myshare/lib/basics/core_notation/compose_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/comprehension_2.ma" {"matita/myshare/lib/basics/core_notation/comprehension_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/downarrow_1.ma" {"matita/myshare/lib/basics/core_notation/downarrow_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/exp_2.ma" {"matita/myshare/lib/basics/core_notation/exp_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/fact_1.ma" {"matita/myshare/lib/basics/core_notation/fact_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/fintersects_2.ma" {"matita/myshare/lib/basics/core_notation/fintersects_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/funion_2.ma" {"matita/myshare/lib/basics/core_notation/funion_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/invert_1.ma" {"matita/myshare/lib/basics/core_notation/invert_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/invert_appl_2.ma" {"matita/myshare/lib/basics/core_notation/invert_appl_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/napart_2.ma" {"matita/myshare/lib/basics/core_notation/napart_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/overlaps_2.ma" {"matita/myshare/lib/basics/core_notation/overlaps_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/pair_2.ma" {"matita/myshare/lib/basics/core_notation/pair_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/singl_1.ma" {"matita/myshare/lib/basics/core_notation/singl_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/subset_1.ma" {"matita/myshare/lib/basics/core_notation/subset_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/subseteq_2.ma" {"matita/myshare/lib/basics/core_notation/subseteq_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/uparrow_1.ma" {"matita/myshare/lib/basics/core_notation/uparrow_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/deqlist.ma" {"matita/myshare/lib/basics/deqlist.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/deqsets.ma" {"matita/myshare/lib/basics/deqsets.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/finset.ma" {"matita/myshare/lib/basics/finset.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/jmeq.ma" {"matita/myshare/lib/basics/jmeq.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/lists/list.ma" {"matita/myshare/lib/basics/lists/list.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/lists/listb.ma" {"matita/myshare/lib/basics/lists/listb.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/lists/lstar.ma" {"matita/myshare/lib/basics/lists/lstar.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/logic.ma" {"matita/myshare/lib/basics/logic.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/pts.ma" {"matita/myshare/lib/basics/pts.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/relations.ma" {"matita/myshare/lib/basics/relations.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/russell.ma" {"matita/myshare/lib/basics/russell.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/sets.ma" {"matita/myshare/lib/basics/sets.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/star.ma" {"matita/myshare/lib/basics/star.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/star1.ma" {"matita/myshare/lib/basics/star1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/types.ma" {"matita/myshare/lib/basics/types.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/vector_finset.ma" {"matita/myshare/lib/basics/vector_finset.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/vectors.ma" {"matita/myshare/lib/basics/vectors.ma"}
+  "_build/install/default/share/matita/myshare/lib/didactic/natural_deduction.ma" {"matita/myshare/lib/didactic/natural_deduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/extraction.ma" {"matita/myshare/lib/extraction.ma"}
+  "_build/install/default/share/matita/myshare/lib/fail.txt" {"matita/myshare/lib/fail.txt"}
+  "_build/install/default/share/matita/myshare/lib/finite_lambda/confluence.ma" {"matita/myshare/lib/finite_lambda/confluence.ma"}
+  "_build/install/default/share/matita/myshare/lib/finite_lambda/reduction.ma" {"matita/myshare/lib/finite_lambda/reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/finite_lambda/terms_and_types.ma" {"matita/myshare/lib/finite_lambda/terms_and_types.ma"}
+  "_build/install/default/share/matita/myshare/lib/finite_lambda/typing.ma" {"matita/myshare/lib/finite_lambda/typing.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/apply_functor.ma" {"matita/myshare/lib/formal_topology/apply_functor.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/basic_pairs.ma" {"matita/myshare/lib/formal_topology/basic_pairs.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/basic_pairs_to_basic_topologies.ma" {"matita/myshare/lib/formal_topology/basic_pairs_to_basic_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma" {"matita/myshare/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/basic_topologies.ma" {"matita/myshare/lib/formal_topology/basic_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma" {"matita/myshare/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/categories.ma" {"matita/myshare/lib/formal_topology/categories.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/concrete_spaces.ma" {"matita/myshare/lib/formal_topology/concrete_spaces.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma" {"matita/myshare/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/cprop_connectives.ma" {"matita/myshare/lib/formal_topology/cprop_connectives.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/formal_topologies.ma" {"matita/myshare/lib/formal_topology/formal_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/notation.ma" {"matita/myshare/lib/formal_topology/notation.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-algebra.ma" {"matita/myshare/lib/formal_topology/o-algebra.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-basic_pairs.ma" {"matita/myshare/lib/formal_topology/o-basic_pairs.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma" {"matita/myshare/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-basic_topologies.ma" {"matita/myshare/lib/formal_topology/o-basic_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-concrete_spaces.ma" {"matita/myshare/lib/formal_topology/o-concrete_spaces.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-formal_topologies.ma" {"matita/myshare/lib/formal_topology/o-formal_topologies.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/o-saturations.ma" {"matita/myshare/lib/formal_topology/o-saturations.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/r-o-basic_pairs.ma" {"matita/myshare/lib/formal_topology/r-o-basic_pairs.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/relations.ma" {"matita/myshare/lib/formal_topology/relations.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/relations_to_o-algebra.ma" {"matita/myshare/lib/formal_topology/relations_to_o-algebra.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/replace.sh" {"matita/myshare/lib/formal_topology/replace.sh"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/saturations.ma" {"matita/myshare/lib/formal_topology/saturations.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/saturations_to_o-saturations.ma" {"matita/myshare/lib/formal_topology/saturations_to_o-saturations.ma"}
+  "_build/install/default/share/matita/myshare/lib/formal_topology/subsets.ma" {"matita/myshare/lib/formal_topology/subsets.ma"}
+  "_build/install/default/share/matita/myshare/lib/hints_declaration.ma" {"matita/myshare/lib/hints_declaration.ma"}
+  "_build/install/default/share/matita/myshare/lib/hott/Overture.ma" {"matita/myshare/lib/hott/Overture.ma"}
+  "_build/install/default/share/matita/myshare/lib/hott/PathGroupoids.ma" {"matita/myshare/lib/hott/PathGroupoids.ma"}
+  "_build/install/default/share/matita/myshare/lib/hott/notations.ma" {"matita/myshare/lib/hott/notations.ma"}
+  "_build/install/default/share/matita/myshare/lib/hott/pts.ma" {"matita/myshare/lib/hott/pts.ma"}
+  "_build/install/default/share/matita/myshare/lib/hott/types.ma" {"matita/myshare/lib/hott/types.ma"}
+  "_build/install/default/share/matita/myshare/lib/inconsistent.ma" {"matita/myshare/lib/inconsistent.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/Makefile" {"matita/myshare/lib/lambda/Makefile"}
+  "_build/install/default/share/matita/myshare/lib/lambda/background/preamble.ma" {"matita/myshare/lib/lambda/background/preamble.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/etc/cons_r.etc" {"matita/myshare/lib/lambda/etc/cons_r.etc"}
+  "_build/install/default/share/matita/myshare/lib/lambda/levels/interpretations.ma" {"matita/myshare/lib/lambda/levels/interpretations.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/levels/iterated_abstraction.ma" {"matita/myshare/lib/lambda/levels/iterated_abstraction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/levels/term.ma" {"matita/myshare/lib/lambda/levels/term.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/abstraction_1.ma" {"matita/myshare/lib/lambda/notation/functions/abstraction_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/abstraction_2.ma" {"matita/myshare/lib/lambda/notation/functions/abstraction_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/annotatedabstraction_2.ma" {"matita/myshare/lib/lambda/notation/functions/annotatedabstraction_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/application_2.ma" {"matita/myshare/lib/lambda/notation/functions/application_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/application_3.ma" {"matita/myshare/lib/lambda/notation/functions/application_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/backward_1.ma" {"matita/myshare/lib/lambda/notation/functions/backward_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/backward_3.ma" {"matita/myshare/lib/lambda/notation/functions/backward_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/dsubst_3.ma" {"matita/myshare/lib/lambda/notation/functions/dsubst_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/forward_1.ma" {"matita/myshare/lib/lambda/notation/functions/forward_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/forward_3.ma" {"matita/myshare/lib/lambda/notation/functions/forward_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/hocons_2.ma" {"matita/myshare/lib/lambda/notation/functions/hocons_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/lift_3.ma" {"matita/myshare/lib/lambda/notation/functions/lift_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/multiplicity_1.ma" {"matita/myshare/lib/lambda/notation/functions/multiplicity_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/nil_0.ma" {"matita/myshare/lib/lambda/notation/functions/nil_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/projectdown_1.ma" {"matita/myshare/lib/lambda/notation/functions/projectdown_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/projectsame_2.ma" {"matita/myshare/lib/lambda/notation/functions/projectsame_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/projectup_2.ma" {"matita/myshare/lib/lambda/notation/functions/projectup_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/variablereferencebyindex_1.ma" {"matita/myshare/lib/lambda/notation/functions/variablereferencebyindex_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/variablereferencebyindex_2.ma" {"matita/myshare/lib/lambda/notation/functions/variablereferencebyindex_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/functions/variablereferencebylevel_2.ma" {"matita/myshare/lib/lambda/notation/functions/variablereferencebylevel_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/decomposedstd_2.ma" {"matita/myshare/lib/lambda/notation/relations/decomposedstd_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/parred_2.ma" {"matita/myshare/lib/lambda/notation/relations/parred_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/parredstar_2.ma" {"matita/myshare/lib/lambda/notation/relations/parredstar_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/prec_2.ma" {"matita/myshare/lib/lambda/notation/relations/prec_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/seqred_2.ma" {"matita/myshare/lib/lambda/notation/relations/seqred_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/seqred_3.ma" {"matita/myshare/lib/lambda/notation/relations/seqred_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/seqredstar_2.ma" {"matita/myshare/lib/lambda/notation/relations/seqredstar_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/seqredstar_3.ma" {"matita/myshare/lib/lambda/notation/relations/seqredstar_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/std_3.ma" {"matita/myshare/lib/lambda/notation/relations/std_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/relations/stdstar_3.ma" {"matita/myshare/lib/lambda/notation/relations/stdstar_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_1_2.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_1_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_2_2.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_2_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_2_3.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_2_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_3_1.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_3_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_3_2.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_3_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_3_3.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_3_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_3_4.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_3_4.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_4_1.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_4_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_4_2.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_4_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/ex_4_3.ma" {"matita/myshare/lib/lambda/notation/xoa/ex_4_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/false_0.ma" {"matita/myshare/lib/lambda/notation/xoa/false_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/or_3.ma" {"matita/myshare/lib/lambda/notation/xoa/or_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/notation/xoa/true_0.ma" {"matita/myshare/lib/lambda/notation/xoa/true_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/alternative_standard_order.ma" {"matita/myshare/lib/lambda/paths/alternative_standard_order.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/decomposed_trace.ma" {"matita/myshare/lib/lambda/paths/decomposed_trace.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/dst_computation.ma" {"matita/myshare/lib/lambda/paths/dst_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/labeled_sequential_computation.ma" {"matita/myshare/lib/lambda/paths/labeled_sequential_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/labeled_sequential_reduction.ma" {"matita/myshare/lib/lambda/paths/labeled_sequential_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/labeled_st_computation.ma" {"matita/myshare/lib/lambda/paths/labeled_st_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/labeled_st_reduction.ma" {"matita/myshare/lib/lambda/paths/labeled_st_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/path.ma" {"matita/myshare/lib/lambda/paths/path.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/standard_order.ma" {"matita/myshare/lib/lambda/paths/standard_order.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/standard_precedence.ma" {"matita/myshare/lib/lambda/paths/standard_precedence.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/standard_trace.ma" {"matita/myshare/lib/lambda/paths/standard_trace.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/paths/trace.ma" {"matita/myshare/lib/lambda/paths/trace.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/policy.txt" {"matita/myshare/lib/lambda/policy.txt"}
+  "_build/install/default/share/matita/myshare/lib/lambda/replace.sh" {"matita/myshare/lib/lambda/replace.sh"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/boolean.ma" {"matita/myshare/lib/lambda/subterms/boolean.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/booleanized.ma" {"matita/myshare/lib/lambda/subterms/booleanized.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/carrier.ma" {"matita/myshare/lib/lambda/subterms/carrier.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/relocating_substitution.ma" {"matita/myshare/lib/lambda/subterms/relocating_substitution.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/relocation.ma" {"matita/myshare/lib/lambda/subterms/relocation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/subterms/subterms.ma" {"matita/myshare/lib/lambda/subterms/subterms.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/iterated_abstraction.ma" {"matita/myshare/lib/lambda/terms/iterated_abstraction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/labeled_sequential_computation.ma" {"matita/myshare/lib/lambda/terms/labeled_sequential_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/multiplicity.ma" {"matita/myshare/lib/lambda/terms/multiplicity.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/parallel_computation.ma" {"matita/myshare/lib/lambda/terms/parallel_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/parallel_reduction.ma" {"matita/myshare/lib/lambda/terms/parallel_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/relocating_substitution.ma" {"matita/myshare/lib/lambda/terms/relocating_substitution.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/relocation.ma" {"matita/myshare/lib/lambda/terms/relocation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/sequential_computation.ma" {"matita/myshare/lib/lambda/terms/sequential_computation.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/sequential_reduction.ma" {"matita/myshare/lib/lambda/terms/sequential_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/size.ma" {"matita/myshare/lib/lambda/terms/size.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/supercombinator.ma" {"matita/myshare/lib/lambda/terms/supercombinator.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/terms/term.ma" {"matita/myshare/lib/lambda/terms/term.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa.conf.xml" {"matita/myshare/lib/lambda/xoa.conf.xml"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_1_2.ma" {"matita/myshare/lib/lambda/xoa/ex_1_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_2_2.ma" {"matita/myshare/lib/lambda/xoa/ex_2_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_2_3.ma" {"matita/myshare/lib/lambda/xoa/ex_2_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_3_1.ma" {"matita/myshare/lib/lambda/xoa/ex_3_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_3_2.ma" {"matita/myshare/lib/lambda/xoa/ex_3_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_3_3.ma" {"matita/myshare/lib/lambda/xoa/ex_3_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_3_4.ma" {"matita/myshare/lib/lambda/xoa/ex_3_4.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_4_1.ma" {"matita/myshare/lib/lambda/xoa/ex_4_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_4_2.ma" {"matita/myshare/lib/lambda/xoa/ex_4_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/ex_4_3.ma" {"matita/myshare/lib/lambda/xoa/ex_4_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/lambda/xoa/or_3.ma" {"matita/myshare/lib/lambda/xoa/or_3.ma"}
+  "_build/install/default/share/matita/myshare/lib/preamble.hs" {"matita/myshare/lib/preamble.hs"}
+  "_build/install/default/share/matita/myshare/lib/preamble.ml" {"matita/myshare/lib/preamble.ml"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/CC2FO_K.ma" {"matita/myshare/lib/pts_dummy/CC2FO_K.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/CC2FO_K_cube.ma" {"matita/myshare/lib/pts_dummy/CC2FO_K_cube.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/arity.ma" {"matita/myshare/lib/pts_dummy/arity.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/arity_eval.ma" {"matita/myshare/lib/pts_dummy/arity_eval.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/convertibility.ma" {"matita/myshare/lib/pts_dummy/convertibility.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/cube.ma" {"matita/myshare/lib/pts_dummy/cube.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/degree.ma" {"matita/myshare/lib/pts_dummy/degree.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/ext.ma" {"matita/myshare/lib/pts_dummy/ext.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/ext_lambda.ma" {"matita/myshare/lib/pts_dummy/ext_lambda.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/inversion.ma" {"matita/myshare/lib/pts_dummy/inversion.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/lambda_notation.ma" {"matita/myshare/lib/pts_dummy/lambda_notation.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/lift.ma" {"matita/myshare/lib/pts_dummy/lift.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/par_reduction.ma" {"matita/myshare/lib/pts_dummy/par_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/rc_eval.ma" {"matita/myshare/lib/pts_dummy/rc_eval.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/rc_hsat.ma" {"matita/myshare/lib/pts_dummy/rc_hsat.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/rc_sat.ma" {"matita/myshare/lib/pts_dummy/rc_sat.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/reduction.ma" {"matita/myshare/lib/pts_dummy/reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/sn.ma" {"matita/myshare/lib/pts_dummy/sn.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/subject.ma" {"matita/myshare/lib/pts_dummy/subject.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/subst.ma" {"matita/myshare/lib/pts_dummy/subst.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/subterms.ma" {"matita/myshare/lib/pts_dummy/subterms.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/terms.ma" {"matita/myshare/lib/pts_dummy/terms.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy/types.ma" {"matita/myshare/lib/pts_dummy/types.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/arity.ma" {"matita/myshare/lib/pts_dummy_new/arity.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/arity_eval.ma" {"matita/myshare/lib/pts_dummy_new/arity_eval.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/convertibility.ma" {"matita/myshare/lib/pts_dummy_new/convertibility.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/cube.ma" {"matita/myshare/lib/pts_dummy_new/cube.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/ext.ma" {"matita/myshare/lib/pts_dummy_new/ext.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/ext_lambda.ma" {"matita/myshare/lib/pts_dummy_new/ext_lambda.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/inversion.ma" {"matita/myshare/lib/pts_dummy_new/inversion.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/lambda_notation.ma" {"matita/myshare/lib/pts_dummy_new/lambda_notation.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/par_reduction.ma" {"matita/myshare/lib/pts_dummy_new/par_reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/rc_eval.ma" {"matita/myshare/lib/pts_dummy_new/rc_eval.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/rc_hsat.ma" {"matita/myshare/lib/pts_dummy_new/rc_hsat.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/rc_sat.ma" {"matita/myshare/lib/pts_dummy_new/rc_sat.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/reduction.ma" {"matita/myshare/lib/pts_dummy_new/reduction.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/sn.ma" {"matita/myshare/lib/pts_dummy_new/sn.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/subject.ma" {"matita/myshare/lib/pts_dummy_new/subject.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/subst.ma" {"matita/myshare/lib/pts_dummy_new/subst.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/subterms.ma" {"matita/myshare/lib/pts_dummy_new/subterms.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/terms.ma" {"matita/myshare/lib/pts_dummy_new/terms.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/thinning.ma" {"matita/myshare/lib/pts_dummy_new/thinning.ma"}
+  "_build/install/default/share/matita/myshare/lib/pts_dummy_new/types.ma" {"matita/myshare/lib/pts_dummy_new/types.ma"}
+  "_build/install/default/share/matita/myshare/lib/re/lang.ma" {"matita/myshare/lib/re/lang.ma"}
+  "_build/install/default/share/matita/myshare/lib/re/moves.ma" {"matita/myshare/lib/re/moves.ma"}
+  "_build/install/default/share/matita/myshare/lib/re/re.ma" {"matita/myshare/lib/re/re.ma"}
+  "_build/install/default/share/matita/myshare/lib/re/reb.ma" {"matita/myshare/lib/re/reb.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/almost.ma" {"matita/myshare/lib/reverse_complexity/almost.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/basics.ma" {"matita/myshare/lib/reverse_complexity/basics.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/big_O.ma" {"matita/myshare/lib/reverse_complexity/big_O.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/bigops_compl.ma" {"matita/myshare/lib/reverse_complexity/bigops_compl.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/complexity.ma" {"matita/myshare/lib/reverse_complexity/complexity.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/gap.ma" {"matita/myshare/lib/reverse_complexity/gap.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/hierarchy.ma" {"matita/myshare/lib/reverse_complexity/hierarchy.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/sigma_diseq.ma" {"matita/myshare/lib/reverse_complexity/sigma_diseq.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/speed_clean.ma" {"matita/myshare/lib/reverse_complexity/speed_clean.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/speed_def.ma" {"matita/myshare/lib/reverse_complexity/speed_def.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/speed_new.ma" {"matita/myshare/lib/reverse_complexity/speed_new.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/speedup.ma" {"matita/myshare/lib/reverse_complexity/speedup.ma"}
+  "_build/install/default/share/matita/myshare/lib/reverse_complexity/toolkit.ma" {"matita/myshare/lib/reverse_complexity/toolkit.ma"}
+  "_build/install/default/share/matita/myshare/lib/root" {"matita/myshare/lib/root"}
+  "_build/install/default/share/matita/myshare/lib/self_typing.ma" {"matita/myshare/lib/self_typing.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/auxiliary_machines.ma" {"matita/myshare/lib/turing/auxiliary_machines.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/auxiliary_machines1.ma" {"matita/myshare/lib/turing/auxiliary_machines1.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/auxiliary_multi_machines.ma" {"matita/myshare/lib/turing/auxiliary_multi_machines.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/basic_machines.ma" {"matita/myshare/lib/turing/basic_machines.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/basic_multi_machines.ma" {"matita/myshare/lib/turing/basic_multi_machines.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/complexity.ma" {"matita/myshare/lib/turing/complexity.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/if_machine.ma" {"matita/myshare/lib/turing/if_machine.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/if_multi.ma" {"matita/myshare/lib/turing/if_multi.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/inject.ma" {"matita/myshare/lib/turing/inject.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/mono.ma" {"matita/myshare/lib/turing/mono.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/move_char.ma" {"matita/myshare/lib/turing/move_char.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/exec_moves.ma" {"matita/myshare/lib/turing/multi_to_mono/exec_moves.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/exec_trace_move.ma" {"matita/myshare/lib/turing/multi_to_mono/exec_trace_move.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/full.ma" {"matita/myshare/lib/turing/multi_to_mono/full.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/shift_trace.ma" {"matita/myshare/lib/turing/multi_to_mono/shift_trace.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/shift_trace_aux.ma" {"matita/myshare/lib/turing/multi_to_mono/shift_trace_aux.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/step.ma" {"matita/myshare/lib/turing/multi_to_mono/step.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_to_mono/trace_alphabet.ma" {"matita/myshare/lib/turing/multi_to_mono/trace_alphabet.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/alphabet.ma" {"matita/myshare/lib/turing/multi_universal/alphabet.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/binaryTM.ma" {"matita/myshare/lib/turing/multi_universal/binaryTM.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/match.ma" {"matita/myshare/lib/turing/multi_universal/match.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/normalTM.ma" {"matita/myshare/lib/turing/multi_universal/normalTM.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/tuples.ma" {"matita/myshare/lib/turing/multi_universal/tuples.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/unistep.ma" {"matita/myshare/lib/turing/multi_universal/unistep.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/unistep_aux.ma" {"matita/myshare/lib/turing/multi_universal/unistep_aux.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/multi_universal/universal.ma" {"matita/myshare/lib/turing/multi_universal/universal.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/ntm.ma" {"matita/myshare/lib/turing/ntm.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/oracle.ma" {"matita/myshare/lib/turing/oracle.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/turing.ma" {"matita/myshare/lib/turing/turing.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/turing_old.ma" {"matita/myshare/lib/turing/turing_old.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/universal.ma" {"matita/myshare/lib/turing/universal.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/while_machine.ma" {"matita/myshare/lib/turing/while_machine.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/while_multi.ma" {"matita/myshare/lib/turing/while_multi.ma"}
+  "_build/install/default/share/matita/myshare/lib/turing/wmono.ma" {"matita/myshare/lib/turing/wmono.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter1.ma" {"matita/myshare/lib/tutorial/chapter1.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter10.ma" {"matita/myshare/lib/tutorial/chapter10.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter11.ma" {"matita/myshare/lib/tutorial/chapter11.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter12.ma" {"matita/myshare/lib/tutorial/chapter12.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter13.ma" {"matita/myshare/lib/tutorial/chapter13.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter2.ma" {"matita/myshare/lib/tutorial/chapter2.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter3.ma" {"matita/myshare/lib/tutorial/chapter3.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter4.ma" {"matita/myshare/lib/tutorial/chapter4.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter5.ma" {"matita/myshare/lib/tutorial/chapter5.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter6.ma" {"matita/myshare/lib/tutorial/chapter6.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter7.ma" {"matita/myshare/lib/tutorial/chapter7.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter8.ma" {"matita/myshare/lib/tutorial/chapter8.ma"}
+  "_build/install/default/share/matita/myshare/lib/tutorial/chapter9.ma" {"matita/myshare/lib/tutorial/chapter9.ma"}
+  "_build/install/default/share/matita/myshare/matita.conf.xml" {"matita/myshare/matita.conf.xml"}
+  "_build/install/default/share/matita/myshare/matita.gtkrc" {"matita/myshare/matita.gtkrc"}
+  "_build/install/default/share/matita/myshare/matita.lang" {"matita/myshare/matita.lang"}
+  "_build/install/default/share/matita/myshare/matita.ma.templ" {"matita/myshare/matita.ma.templ"}
 ]

diff --git a/matita/matita.opam b/matita/matita.opam
index e235ed50d759f16cc54dd9390219d2551af55c5f..f2e62ac09ebee07caa97309541973daa992e72ed 100644 (file)
--- a/matita/matita.opam
+++ b/matita/matita.opam
@@ -19,6 +19,8 @@ depends: [
   "ulex-camlp5" {= "1.3"}
   "ocaml-expat" {= "1.1.0"}
   "lablgtk3-sourceview3" {= "3.1.3"}
+  "dune-build-info"
+  "dune-site"
   "camlp5" {= "8.00.04"}
   "odoc" {with-doc}
 ]
@@ -31,9 +33,11 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git://matita.cs.unibo.it/git/helm"

diff --git a/matita/matita/buildTimeConf.ml b/matita/matita/buildTimeConf.ml
index fab7db0cdb97d4ae6f61fa827f6338962835c6b6..3774aaf35a9087358926efa5da731ec4c43d4a99 100644 (file)
--- a/matita/matita/buildTimeConf.ml
+++ b/matita/matita/buildTimeConf.ml
@@ -40,7 +40,10 @@ let script_font = "Monospace";;
 let runtime_base_dir =
   try
     Sys.getenv "MATITA_RT_BASE_DIR"
-  with Not_found -> "/home/claudio/ricerca/matita5/helm/matita/matita";;
+  with Not_found ->
+   match Mysites.Sites.myshare with
+      [rt] -> rt (*It was: "/home/claudio/ricerca/matita5/helm/matita/matita"*)
+    | _ -> assert false
 
 let images_dir = runtime_base_dir ^ "/icons"
 let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc"

diff --git a/matita/matita/dune b/matita/matita/dune
index 55983d8e6bc40dbffd37ed7edda32a0d2a428834..f1798f02010ebb73275fa5efbcc0646eba40c5da 100644 (file)
--- a/matita/matita/dune
+++ b/matita/matita/dune
@@ -1,9 +1,13 @@
 (library
  (name matita_cli)
  (wrapped false)
- (libraries helm_grafite_engine lablgtk3-sourceview3 dune-build-info)
+ (libraries helm_grafite_engine lablgtk3-sourceview3 dune-build-info dune-site)
  (modules 
-   buildTimeConf matitaTypes matitaMiscCli applyTransformation matitaEngine matitaExcPp matitaInit))
+   mysites buildTimeConf matitaTypes matitaMiscCli applyTransformation matitaEngine matitaExcPp matitaInit))
+
+(generate_sites_module
+ (module mysites)
+ (sites matita))
 
 (executable
  (name matita)
@@ -22,7 +26,7 @@
  (modules matitac matitaclean))
 
 (install
- (section share)
+ (section (site (matita myshare)))
  (files
   (glob_files_rec lib/*)
   (glob_files_rec help/*) ; brutal

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 88f5cb380fa82ba395e5d3aa883c5632b7fc76c9..e05d4c41c5fe7639998f5633ccc7ea903525d183 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -672,6 +672,7 @@ class gui () =
         ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
+      console#message (sprintf "\tStandard library location:\n\t  %s\n" BuildTimeConf.new_stdlib_dir_devel);
         (* natural deduction palette *)
       main#tacticsButtonsHandlebox#misc#hide ();
       MatitaGtkMisc.toggle_callback