From 791d52ba005e434be27cca1f8059d9f28da0183b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 10:12:15 +0000 Subject: [PATCH] - lexicon merged into ng_disambiguation --- .../METAS/meta.helm-grafite_parser.src | 2 +- matita/components/METAS/meta.helm-lexicon.src | 4 -- .../METAS/meta.helm-ng_cic_content.src | 2 +- .../components/METAS/meta.helm-ng_library.src | 2 +- .../components/METAS/meta.helm-ng_tactics.src | 2 +- matita/components/Makefile | 3 +- matita/components/content/.depend.opt | 9 ++-- matita/components/content_pres/.depend.opt | 4 +- matita/components/extlib/.depend.opt | 3 -- matita/components/grafite/.depend.opt | 3 -- matita/components/grafite_engine/.depend.opt | 7 +-- matita/components/grafite_parser/.depend.opt | 3 -- matita/components/lexicon/.depend | 6 --- matita/components/lexicon/.depend.opt | 21 --------- matita/components/lexicon/Makefile | 12 ----- matita/components/ng_cic_content/.depend.opt | 6 +-- matita/components/ng_disambiguation/.depend | 11 ++++- .../components/ng_disambiguation/.depend.opt | 13 +++++- matita/components/ng_disambiguation/Makefile | 46 ++++--------------- .../grafiteDisambiguate.ml | 0 .../grafiteDisambiguate.mli | 0 .../ng_disambiguation/nnumber_notation.mli | 28 +++++++++++ matita/components/ng_refiner/.depend.opt | 7 +-- matita/components/ng_tactics/.depend.opt | 2 +- 24 files changed, 74 insertions(+), 122 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-lexicon.src delete mode 100644 matita/components/lexicon/.depend delete mode 100644 matita/components/lexicon/.depend.opt delete mode 100644 matita/components/lexicon/Makefile rename matita/components/{lexicon => ng_disambiguation}/grafiteDisambiguate.ml (100%) rename matita/components/{lexicon => ng_disambiguation}/grafiteDisambiguate.mli (100%) create mode 100644 matita/components/ng_disambiguation/nnumber_notation.mli diff --git a/matita/components/METAS/meta.helm-grafite_parser.src b/matita/components/METAS/meta.helm-grafite_parser.src index bcde338d3..91bfdab4c 100644 --- a/matita/components/METAS/meta.helm-grafite_parser.src +++ b/matita/components/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation helm-ng_library" +requires="helm-grafite ulex08 helm-ng_disambiguation helm-ng_library helm-content_pres" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/matita/components/METAS/meta.helm-lexicon.src b/matita/components/METAS/meta.helm-lexicon.src deleted file mode 100644 index 0842312ec..000000000 --- a/matita/components/METAS/meta.helm-lexicon.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-content_pres helm-ng_library camlp5.gramlib" -version="0.0.1" -archive(byte)="lexicon.cma" -archive(native)="lexicon.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_cic_content.src b/matita/components/METAS/meta.helm-ng_cic_content.src index a2c08e135..1b45e784a 100644 --- a/matita/components/METAS/meta.helm-ng_cic_content.src +++ b/matita/components/METAS/meta.helm-ng_cic_content.src @@ -1,4 +1,4 @@ -requires="helm-library helm-content helm-ng_refiner" +requires="helm-library helm-ng_library helm-grafite helm-content helm-ng_refiner" version="0.0.1" archive(byte)="ng_cic_content.cma" archive(native)="ng_cic_content.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_library.src b/matita/components/METAS/meta.helm-ng_library.src index ebe2e340e..a40447075 100644 --- a/matita/components/METAS/meta.helm-ng_library.src +++ b/matita/components/METAS/meta.helm-ng_library.src @@ -1,4 +1,4 @@ -requires="helm-ng_refiner helm-ng_cic_content helm-ng_disambiguation helm-ng_paramodulation" +requires="helm-ng_refiner helm-registry helm-library" version="0.0.1" archive(byte)="ng_library.cma" archive(native)="ng_library.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_tactics.src b/matita/components/METAS/meta.helm-ng_tactics.src index 4a8eca4b1..f5d3a660d 100644 --- a/matita/components/METAS/meta.helm-ng_tactics.src +++ b/matita/components/METAS/meta.helm-ng_tactics.src @@ -1,4 +1,4 @@ -requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-ng_paramodulation" +requires="helm-ng_disambiguation helm-grafite_parser helm-ng_paramodulation" version="0.0.1" archive(byte)="ng_tactics.cma" archive(native)="ng_tactics.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index b1485c5cf..61ce8a364 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -18,13 +18,12 @@ MODULES = \ content \ grafite \ ng_refiner \ + ng_library \ ng_cic_content \ disambiguation \ ng_disambiguation \ ng_paramodulation \ - ng_library \ content_pres \ - lexicon \ grafite_parser \ ng_tactics \ grafite_engine \ diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index a964a1fca..34a327264 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,8 +1,7 @@ content.cmi: -notationUtil.cmi: -notationEnv.cmi: -notationPp.cmi: -interpretations.cmi: notationPt.cmx +notationUtil.cmi: notationPt.cmx +notationEnv.cmi: notationPt.cmx +notationPp.cmi: notationPt.cmx notationEnv.cmi notationPt.cmo: notationPt.cmx: content.cmo: content.cmi @@ -13,5 +12,3 @@ notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi -interpretations.cmo: notationUtil.cmi notationPt.cmx interpretations.cmi -interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 8d74439eb..7b0acd5dc 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -7,8 +7,8 @@ content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi -content2pres.cmi: cicNotationPres.cmi -sequent2pres.cmi: cicNotationPres.cmi +content2pres.cmi: termContentPres.cmi cicNotationPres.cmi +sequent2pres.cmi: termContentPres.cmi cicNotationPres.cmi renderingAttrs.cmo: renderingAttrs.cmi renderingAttrs.cmx: renderingAttrs.cmi cicNotationLexer.cmo: cicNotationLexer.cmi diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index dcc6377a0..f6168c1bc 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -6,7 +6,6 @@ hLog.cmi: trie.cmi: discrimination_tree.cmi: hTopoSort.cmi: -refCounter.cmi: graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi @@ -24,7 +23,5 @@ discrimination_tree.cmo: trie.cmi discrimination_tree.cmi discrimination_tree.cmx: trie.cmx discrimination_tree.cmi hTopoSort.cmo: hTopoSort.cmi hTopoSort.cmx: hTopoSort.cmi -refCounter.cmo: refCounter.cmi -refCounter.cmx: refCounter.cmi graphvizPp.cmo: graphvizPp.cmi graphvizPp.cmx: graphvizPp.cmi diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index e01d5bbfa..3a2590d84 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,8 +1,5 @@ grafiteAstPp.cmi: grafiteAst.cmx -grafiteMarshal.cmi: grafiteAst.cmx grafiteAst.cmo: grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi -grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi -grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 10236823a..d04ec9d2c 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,14 +1,11 @@ grafiteTypes.cmi: -grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi grafiteTypes.cmx: grafiteTypes.cmi -grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi -grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi -grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi grafiteSync.cmi \ +grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \ grafiteEngine.cmi -grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx grafiteSync.cmx \ +grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \ grafiteEngine.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e45f9bef8..b8b65a8c0 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,12 +1,9 @@ dependenciesParser.cmi: grafiteParser.cmi: -grafiteDisambiguate.cmi: print_grammar.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi print_grammar.cmx: print_grammar.cmi diff --git a/matita/components/lexicon/.depend b/matita/components/lexicon/.depend deleted file mode 100644 index 84cbde3e1..000000000 --- a/matita/components/lexicon/.depend +++ /dev/null @@ -1,6 +0,0 @@ -grafiteDisambiguate.cmi: -lexiconSync.cmi: grafiteDisambiguate.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi -lexiconSync.cmo: grafiteDisambiguate.cmi lexiconSync.cmi -lexiconSync.cmx: grafiteDisambiguate.cmx lexiconSync.cmi diff --git a/matita/components/lexicon/.depend.opt b/matita/components/lexicon/.depend.opt deleted file mode 100644 index 0fee4b18e..000000000 --- a/matita/components/lexicon/.depend.opt +++ /dev/null @@ -1,21 +0,0 @@ -lexiconAstPp.cmi: lexiconAst.cmx -lexiconMarshal.cmi: lexiconAst.cmx -cicNotation.cmi: lexiconAst.cmx -lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi -lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx -lexiconAst.cmo: -lexiconAst.cmx: -lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi -lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi -lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi -lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi -cicNotation.cmo: lexiconAst.cmx cicNotation.cmi -cicNotation.cmx: lexiconAst.cmx cicNotation.cmi -lexiconEngine.cmo: lexiconMarshal.cmi lexiconAstPp.cmi lexiconAst.cmx \ - cicNotation.cmi lexiconEngine.cmi -lexiconEngine.cmx: lexiconMarshal.cmx lexiconAstPp.cmx lexiconAst.cmx \ - cicNotation.cmx lexiconEngine.cmi -lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmx cicNotation.cmi \ - lexiconSync.cmi -lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \ - lexiconSync.cmi diff --git a/matita/components/lexicon/Makefile b/matita/components/lexicon/Makefile deleted file mode 100644 index 273aade43..000000000 --- a/matita/components/lexicon/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -PACKAGE = lexicon -PREDICATES = - -INTERFACE_FILES = \ - grafiteDisambiguate.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index 1316c8eab..fd1b831b9 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,6 +1,6 @@ ncic2astMatcher.cmi: -nTermCicContent.cmi: +interpretations.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi -nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi -nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi +interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend index a520f2c39..df0847b17 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -1,7 +1,14 @@ +disambiguateChoices.cmi: nCicDisambiguate.cmi: +nnumber_notation.cmi: +grafiteDisambiguate.cmi: disambiguateChoices.cmo: disambiguateChoices.cmi disambiguateChoices.cmx: disambiguateChoices.cmi nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi -nnumber_notation.cmo: disambiguateChoices.cmi -nnumber_notation.cmx: disambiguateChoices.cmx +nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi +nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi +grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ + grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ + grafiteDisambiguate.cmi diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index f2694c199..df0847b17 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,5 +1,14 @@ +disambiguateChoices.cmi: nCicDisambiguate.cmi: +nnumber_notation.cmi: +grafiteDisambiguate.cmi: +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi -nnumber_notation.cmo: -nnumber_notation.cmx: +nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi +nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi +grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ + grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ + grafiteDisambiguate.cmi diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile index ad6a6de80..8c564325e 100644 --- a/matita/components/ng_disambiguation/Makefile +++ b/matita/components/ng_disambiguation/Makefile @@ -1,45 +1,15 @@ PACKAGE = ng_disambiguation PREDICATES = -INTERFACE_FILES = nCicDisambiguate.mli +INTERFACE_FILES = \ + disambiguateChoices.mli \ + nCicDisambiguate.mli \ + nnumber_notation.mli \ + grafiteDisambiguate.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) -IMPLEMENTATION_FILES = \ - disambiguateChoices.ml \ - $(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae - -all: -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - -depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) - ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot - tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot - cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot . - echo "NCicLibrary [ style=dashed ];" >> depend.dot - echo "NCicPp [ style=dashed ];" >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot . - -depend.png depend.eps: depend.dot - dot -Tpng > depend.png < depend.dot - dot -Tps > depend.eps < depend.dot include ../../Makefile.defs include ../Makefile.common - -OCAMLARCHIVEOPTIONS += -linkall diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml similarity index 100% rename from matita/components/lexicon/grafiteDisambiguate.ml rename to matita/components/ng_disambiguation/grafiteDisambiguate.ml diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/ng_disambiguation/grafiteDisambiguate.mli similarity index 100% rename from matita/components/lexicon/grafiteDisambiguate.mli rename to matita/components/ng_disambiguation/grafiteDisambiguate.mli diff --git a/matita/components/ng_disambiguation/nnumber_notation.mli b/matita/components/ng_disambiguation/nnumber_notation.mli new file mode 100644 index 000000000..91cba3b7c --- /dev/null +++ b/matita/components/ng_disambiguation/nnumber_notation.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *) + +(* Works by side-effects only *) diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index da0ab80fc..2633e1aba 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -2,10 +2,9 @@ nDiscriminationTree.cmi: nCicMetaSubst.cmi: nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi -nRstatus.cmi: nCicCoercion.cmi nCicRefineUtil.cmi: -nCicUnification.cmi: nRstatus.cmi -nCicRefiner.cmi: nRstatus.cmi +nCicUnification.cmi: nCicCoercion.cmi +nCicRefiner.cmi: nCicCoercion.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi @@ -16,8 +15,6 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ nCicCoercion.cmi -nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi -nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index a90df82fa..47f203f0a 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -2,7 +2,7 @@ continuationals.cmi: nCicTacReduction.cmi: nTacStatus.cmi: continuationals.cmi nCicElim.cmi: -nTactics.cmi: nTacStatus.cmi continuationals.cmi +nTactics.cmi: nTacStatus.cmi nnAuto.cmi: nTacStatus.cmi nDestructTac.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi -- 2.39.2