diff --git a/components/binaries/Makefile b/components/binaries/Makefile index 2f2faf326..382bf77db 100644 --- a/components/binaries/Makefile +++ b/components/binaries/Makefile @@ -1,9 +1,9 @@ H=@ -#CSC: saturate is broken after the huge refactoring of auto/paramodulation -#CSC: by Andrea -#BINARIES=extractor table_creator utilities saturate transcript -#FG: my binaries +#FG matex renders lamdba-terms to LaTeX +#FG matitadep exports the dependencies of .ma files +#FG probe returns statistics on compiled files +#FG xoa generates matita files for n-ary logical operators/quantifiers BINARIES=matex matitadep probe xoa all: $(BINARIES:%=rec@all@%) diff --git a/components/broken_binaries/Makefile b/components/broken_binaries/Makefile new file mode 100644 index 000000000..893328c4f --- /dev/null +++ b/components/broken_binaries/Makefile @@ -0,0 +1,18 @@ +H=@ + +#CSC: saturate is broken after the huge refactoring of auto/paramodulation +#CSC: by Andrea +#CSC: the others have not been maintained for a while or they are now useless +BINARIES= + +all: $(BINARIES:%=rec@all@%) +opt: $(BINARIES:%=rec@opt@%) +depend: $(BINARIES:%=rec@depend@%) +depend.opt: $(BINARIES:%=rec@depend.opt@%) +install: $(BINARIES:%=rec@install@%) +uninstall: $(BINARIES:%=rec@uninstall@%) +clean: $(BINARIES:%=rec@clean@%) + +rec@%: + $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) + diff --git a/components/broken_binaries/Makefile.common b/components/broken_binaries/Makefile.common new file mode 100644 index 000000000..78733ed39 --- /dev/null +++ b/components/broken_binaries/Makefile.common @@ -0,0 +1,25 @@ +H=@ + +include ../../../Makefile.defs + +DIST=$(EXEC)---$(VERSION) +DATE=$(shell date +%y%m%d) + +OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) + +opt: + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" $(EXEC).native + +clean: + ocamlbuild -clean + rm -rf $(DIST) $(DIST).tgz + +dist: + mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) + cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources + cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) + tar -cvzf $(DIST).tgz $(DIST) diff --git a/components/binaries/dump_db/dump.sh b/components/broken_binaries/dump_db/dump.sh similarity index 100% rename from components/binaries/dump_db/dump.sh rename to components/broken_binaries/dump_db/dump.sh diff --git a/components/binaries/matitaprover/CASC_2008 b/components/broken_binaries/matitaprover/CASC_2008 similarity index 100% rename from components/binaries/matitaprover/CASC_2008 rename to components/broken_binaries/matitaprover/CASC_2008 diff --git a/components/binaries/matitaprover/FIXME b/components/broken_binaries/matitaprover/FIXME similarity index 100% rename from components/binaries/matitaprover/FIXME rename to components/broken_binaries/matitaprover/FIXME diff --git a/components/binaries/matitaprover/Makefile b/components/broken_binaries/matitaprover/Makefile similarity index 100% rename from components/binaries/matitaprover/Makefile rename to components/broken_binaries/matitaprover/Makefile diff --git a/components/binaries/matitaprover/SystemDescriptionMatita.html b/components/broken_binaries/matitaprover/SystemDescriptionMatita.html similarity index 100% rename from components/binaries/matitaprover/SystemDescriptionMatita.html rename to components/broken_binaries/matitaprover/SystemDescriptionMatita.html diff --git a/components/binaries/matitaprover/TreeLimitedRun.c b/components/broken_binaries/matitaprover/TreeLimitedRun.c similarity index 100% rename from components/binaries/matitaprover/TreeLimitedRun.c rename to components/broken_binaries/matitaprover/TreeLimitedRun.c diff --git a/components/binaries/matitaprover/Veloci b/components/broken_binaries/matitaprover/Veloci similarity index 100% rename from components/binaries/matitaprover/Veloci rename to components/broken_binaries/matitaprover/Veloci diff --git a/components/binaries/matitaprover/_tags b/components/broken_binaries/matitaprover/_tags similarity index 100% rename from components/binaries/matitaprover/_tags rename to components/broken_binaries/matitaprover/_tags diff --git a/components/binaries/matitaprover/ast.ml b/components/broken_binaries/matitaprover/ast.ml similarity index 100% rename from components/binaries/matitaprover/ast.ml rename to components/broken_binaries/matitaprover/ast.ml diff --git a/components/binaries/matitaprover/benchmarks/andrea_log090729 b/components/broken_binaries/matitaprover/benchmarks/andrea_log090729 similarity index 100% rename from components/binaries/matitaprover/benchmarks/andrea_log090729 rename to components/broken_binaries/matitaprover/benchmarks/andrea_log090729 diff --git a/components/binaries/matitaprover/benchmarks/log.090625 b/components/broken_binaries/matitaprover/benchmarks/log.090625 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090625 rename to components/broken_binaries/matitaprover/benchmarks/log.090625 diff --git a/components/binaries/matitaprover/benchmarks/log.090627 b/components/broken_binaries/matitaprover/benchmarks/log.090627 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090627 rename to components/broken_binaries/matitaprover/benchmarks/log.090627 diff --git a/components/binaries/matitaprover/benchmarks/log.090629 b/components/broken_binaries/matitaprover/benchmarks/log.090629 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090629 rename to components/broken_binaries/matitaprover/benchmarks/log.090629 diff --git a/components/binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 b/components/broken_binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 rename to components/broken_binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 diff --git a/components/binaries/matitaprover/benchmarks/log.180CPU.reference b/components/broken_binaries/matitaprover/benchmarks/log.180CPU.reference similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.180CPU.reference rename to components/broken_binaries/matitaprover/benchmarks/log.180CPU.reference diff --git a/components/binaries/matitaprover/benchmarks/log.90.fixed-order b/components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.fixed-order rename to components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order diff --git a/components/binaries/matitaprover/benchmarks/log.90.fixed-order.2 b/components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order.2 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.fixed-order.2 rename to components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order.2 diff --git a/components/binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 b/components/broken_binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 rename to components/broken_binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 diff --git a/components/binaries/matitaprover/casc_2008 b/components/broken_binaries/matitaprover/casc_2008 similarity index 100% rename from components/binaries/matitaprover/casc_2008 rename to components/broken_binaries/matitaprover/casc_2008 diff --git a/components/binaries/matitaprover/discrimination_tree.ml b/components/broken_binaries/matitaprover/discrimination_tree.ml similarity index 100% rename from components/binaries/matitaprover/discrimination_tree.ml rename to components/broken_binaries/matitaprover/discrimination_tree.ml diff --git a/components/binaries/matitaprover/discrimination_tree.mli b/components/broken_binaries/matitaprover/discrimination_tree.mli similarity index 100% rename from components/binaries/matitaprover/discrimination_tree.mli rename to components/broken_binaries/matitaprover/discrimination_tree.mli diff --git a/components/binaries/matitaprover/eligible_unit_equality_problems b/components/broken_binaries/matitaprover/eligible_unit_equality_problems similarity index 100% rename from components/binaries/matitaprover/eligible_unit_equality_problems rename to components/broken_binaries/matitaprover/eligible_unit_equality_problems diff --git a/components/binaries/matitaprover/foSubst.ml b/components/broken_binaries/matitaprover/foSubst.ml similarity index 100% rename from components/binaries/matitaprover/foSubst.ml rename to components/broken_binaries/matitaprover/foSubst.ml diff --git a/components/binaries/matitaprover/foSubst.mli b/components/broken_binaries/matitaprover/foSubst.mli similarity index 100% rename from components/binaries/matitaprover/foSubst.mli rename to components/broken_binaries/matitaprover/foSubst.mli diff --git a/components/binaries/matitaprover/foUnif.ml b/components/broken_binaries/matitaprover/foUnif.ml similarity index 100% rename from components/binaries/matitaprover/foUnif.ml rename to components/broken_binaries/matitaprover/foUnif.ml diff --git a/components/binaries/matitaprover/foUnif.mli b/components/broken_binaries/matitaprover/foUnif.mli similarity index 100% rename from components/binaries/matitaprover/foUnif.mli rename to components/broken_binaries/matitaprover/foUnif.mli diff --git a/components/binaries/matitaprover/foUtils.ml b/components/broken_binaries/matitaprover/foUtils.ml similarity index 100% rename from components/binaries/matitaprover/foUtils.ml rename to components/broken_binaries/matitaprover/foUtils.ml diff --git a/components/binaries/matitaprover/foUtils.mli b/components/broken_binaries/matitaprover/foUtils.mli similarity index 100% rename from components/binaries/matitaprover/foUtils.mli rename to components/broken_binaries/matitaprover/foUtils.mli diff --git a/components/binaries/matitaprover/hExtlib.ml b/components/broken_binaries/matitaprover/hExtlib.ml similarity index 100% rename from components/binaries/matitaprover/hExtlib.ml rename to components/broken_binaries/matitaprover/hExtlib.ml diff --git a/components/binaries/matitaprover/hExtlib.mli b/components/broken_binaries/matitaprover/hExtlib.mli similarity index 100% rename from components/binaries/matitaprover/hExtlib.mli rename to components/broken_binaries/matitaprover/hExtlib.mli diff --git a/components/binaries/matitaprover/hTopoSort.ml b/components/broken_binaries/matitaprover/hTopoSort.ml similarity index 100% rename from components/binaries/matitaprover/hTopoSort.ml rename to components/broken_binaries/matitaprover/hTopoSort.ml diff --git a/components/binaries/matitaprover/hTopoSort.mli b/components/broken_binaries/matitaprover/hTopoSort.mli similarity index 100% rename from components/binaries/matitaprover/hTopoSort.mli rename to components/broken_binaries/matitaprover/hTopoSort.mli diff --git a/components/binaries/matitaprover/index.ml b/components/broken_binaries/matitaprover/index.ml similarity index 100% rename from components/binaries/matitaprover/index.ml rename to components/broken_binaries/matitaprover/index.ml diff --git a/components/binaries/matitaprover/index.mli b/components/broken_binaries/matitaprover/index.mli similarity index 100% rename from components/binaries/matitaprover/index.mli rename to components/broken_binaries/matitaprover/index.mli diff --git a/components/binaries/matitaprover/lexer.mll b/components/broken_binaries/matitaprover/lexer.mll similarity index 100% rename from components/binaries/matitaprover/lexer.mll rename to components/broken_binaries/matitaprover/lexer.mll diff --git a/components/binaries/matitaprover/matitaprover.ml b/components/broken_binaries/matitaprover/matitaprover.ml similarity index 100% rename from components/binaries/matitaprover/matitaprover.ml rename to components/broken_binaries/matitaprover/matitaprover.ml diff --git a/components/binaries/matitaprover/orderings.ml b/components/broken_binaries/matitaprover/orderings.ml similarity index 100% rename from components/binaries/matitaprover/orderings.ml rename to components/broken_binaries/matitaprover/orderings.ml diff --git a/components/binaries/matitaprover/orderings.mli b/components/broken_binaries/matitaprover/orderings.mli similarity index 100% rename from components/binaries/matitaprover/orderings.mli rename to components/broken_binaries/matitaprover/orderings.mli diff --git a/components/binaries/matitaprover/paramod.ml b/components/broken_binaries/matitaprover/paramod.ml similarity index 100% rename from components/binaries/matitaprover/paramod.ml rename to components/broken_binaries/matitaprover/paramod.ml diff --git a/components/binaries/matitaprover/paramod.mli b/components/broken_binaries/matitaprover/paramod.mli similarity index 100% rename from components/binaries/matitaprover/paramod.mli rename to components/broken_binaries/matitaprover/paramod.mli diff --git a/components/binaries/matitaprover/parser.mly b/components/broken_binaries/matitaprover/parser.mly similarity index 100% rename from components/binaries/matitaprover/parser.mly rename to components/broken_binaries/matitaprover/parser.mly diff --git a/components/binaries/matitaprover/pp.ml b/components/broken_binaries/matitaprover/pp.ml similarity index 100% rename from components/binaries/matitaprover/pp.ml rename to components/broken_binaries/matitaprover/pp.ml diff --git a/components/binaries/matitaprover/pp.mli b/components/broken_binaries/matitaprover/pp.mli similarity index 100% rename from components/binaries/matitaprover/pp.mli rename to components/broken_binaries/matitaprover/pp.mli diff --git a/components/binaries/matitaprover/run_on_a_list.sh b/components/broken_binaries/matitaprover/run_on_a_list.sh similarity index 100% rename from components/binaries/matitaprover/run_on_a_list.sh rename to components/broken_binaries/matitaprover/run_on_a_list.sh diff --git a/components/binaries/matitaprover/stats.ml b/components/broken_binaries/matitaprover/stats.ml similarity index 100% rename from components/binaries/matitaprover/stats.ml rename to components/broken_binaries/matitaprover/stats.ml diff --git a/components/binaries/matitaprover/stats.mli b/components/broken_binaries/matitaprover/stats.mli similarity index 100% rename from components/binaries/matitaprover/stats.mli rename to components/broken_binaries/matitaprover/stats.mli diff --git a/components/binaries/matitaprover/stdpp.ml b/components/broken_binaries/matitaprover/stdpp.ml similarity index 100% rename from components/binaries/matitaprover/stdpp.ml rename to components/broken_binaries/matitaprover/stdpp.ml diff --git a/components/binaries/matitaprover/sum_up.awk b/components/broken_binaries/matitaprover/sum_up.awk similarity index 100% rename from components/binaries/matitaprover/sum_up.awk rename to components/broken_binaries/matitaprover/sum_up.awk diff --git a/components/binaries/matitaprover/superposition.ml b/components/broken_binaries/matitaprover/superposition.ml similarity index 100% rename from components/binaries/matitaprover/superposition.ml rename to components/broken_binaries/matitaprover/superposition.ml diff --git a/components/binaries/matitaprover/superposition.mli b/components/broken_binaries/matitaprover/superposition.mli similarity index 100% rename from components/binaries/matitaprover/superposition.mli rename to components/broken_binaries/matitaprover/superposition.mli diff --git a/components/binaries/matitaprover/terms.ml b/components/broken_binaries/matitaprover/terms.ml similarity index 100% rename from components/binaries/matitaprover/terms.ml rename to components/broken_binaries/matitaprover/terms.ml diff --git a/components/binaries/matitaprover/terms.mli b/components/broken_binaries/matitaprover/terms.mli similarity index 100% rename from components/binaries/matitaprover/terms.mli rename to components/broken_binaries/matitaprover/terms.mli diff --git a/components/binaries/matitaprover/tptp_cnf.ml b/components/broken_binaries/matitaprover/tptp_cnf.ml similarity index 100% rename from components/binaries/matitaprover/tptp_cnf.ml rename to components/broken_binaries/matitaprover/tptp_cnf.ml diff --git a/components/binaries/matitaprover/tptp_cnf.mli b/components/broken_binaries/matitaprover/tptp_cnf.mli similarity index 100% rename from components/binaries/matitaprover/tptp_cnf.mli rename to components/broken_binaries/matitaprover/tptp_cnf.mli diff --git a/components/binaries/matitaprover/trie.ml b/components/broken_binaries/matitaprover/trie.ml similarity index 100% rename from components/binaries/matitaprover/trie.ml rename to components/broken_binaries/matitaprover/trie.ml diff --git a/components/binaries/matitaprover/trie.mli b/components/broken_binaries/matitaprover/trie.mli similarity index 100% rename from components/binaries/matitaprover/trie.mli rename to components/broken_binaries/matitaprover/trie.mli diff --git a/components/binaries/saturate/Makefile b/components/broken_binaries/saturate/Makefile similarity index 100% rename from components/binaries/saturate/Makefile rename to components/broken_binaries/saturate/Makefile diff --git a/components/binaries/saturate/saturate_main.ml b/components/broken_binaries/saturate/saturate_main.ml similarity index 100% rename from components/binaries/saturate/saturate_main.ml rename to components/broken_binaries/saturate/saturate_main.ml diff --git a/components/binaries/test_lexer/Makefile b/components/broken_binaries/test_lexer/Makefile similarity index 100% rename from components/binaries/test_lexer/Makefile rename to components/broken_binaries/test_lexer/Makefile diff --git a/components/binaries/test_lexer/test_lexer.ml b/components/broken_binaries/test_lexer/test_lexer.ml similarity index 100% rename from components/binaries/test_lexer/test_lexer.ml rename to components/broken_binaries/test_lexer/test_lexer.ml diff --git a/components/binaries/test_parser/Makefile b/components/broken_binaries/test_parser/Makefile similarity index 100% rename from components/binaries/test_parser/Makefile rename to components/broken_binaries/test_parser/Makefile diff --git a/components/binaries/test_parser/test_dep.ml b/components/broken_binaries/test_parser/test_dep.ml similarity index 100% rename from components/binaries/test_parser/test_dep.ml rename to components/broken_binaries/test_parser/test_dep.ml diff --git a/components/binaries/test_parser/test_parser.ml b/components/broken_binaries/test_parser/test_parser.ml similarity index 100% rename from components/binaries/test_parser/test_parser.ml rename to components/broken_binaries/test_parser/test_parser.ml diff --git a/matita.install b/matita.install index b37e55e1e..658000ffd 100644 --- a/matita.install +++ b/matita.install @@ -93,22 +93,36 @@ share_root: [ "_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/complexes_0.ma" {"matita/myshare/lib/basics/core_notation/complexes_0.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/compose_5.ma" {"matita/myshare/lib/basics/core_notation/compose_5.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/eq_3.ma" {"matita/myshare/lib/basics/core_notation/eq_3.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/hide_1.ma" {"matita/myshare/lib/basics/core_notation/hide_1.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/imply_2.ma" {"matita/myshare/lib/basics/core_notation/imply_2.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/integers_0.ma" {"matita/myshare/lib/basics/core_notation/integers_0.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/naturals_0.ma" {"matita/myshare/lib/basics/core_notation/naturals_0.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/neutral_0.ma" {"matita/myshare/lib/basics/core_notation/neutral_0.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/product_2.ma" {"matita/myshare/lib/basics/core_notation/product_2.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/rationals_0.ma" {"matita/myshare/lib/basics/core_notation/rationals_0.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/reals_0.ma" {"matita/myshare/lib/basics/core_notation/reals_0.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/sqrt_1.ma" {"matita/myshare/lib/basics/core_notation/sqrt_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/uminus_1.ma" {"matita/myshare/lib/basics/core_notation/uminus_1.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/core_notation/vdash_1.ma" {"matita/myshare/lib/basics/core_notation/vdash_1.ma"} + "_build/install/default/share/matita/myshare/lib/basics/core_notation/vdash_3.ma" {"matita/myshare/lib/basics/core_notation/vdash_3.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"}