From f4d41a527321e5fbdc10054b46ad60fe9f7f54a1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 12:39:24 +0000 Subject: [PATCH] cic_disambiguation splitted into disambiguation and cic_disambiguation --- .../METAS/meta.helm-cic_disambiguation.src | 2 +- helm/software/components/Makefile | 1 + .../components/cic_disambiguation/.depend | 21 ++++---------- .../components/cic_disambiguation/Makefile | 13 --------- .../components/disambiguation/Makefile | 28 +++++++++++++++++++ .../disambiguate.crit2.ml | 0 .../disambiguate.crit4.ml | 0 .../disambiguate.ml | 0 .../disambiguate.mli | 0 .../disambiguateTypes.ml | 0 .../disambiguateTypes.mli | 0 helm/software/configure.ac | 2 ++ 12 files changed, 38 insertions(+), 29 deletions(-) create mode 100644 helm/software/components/disambiguation/Makefile rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguate.crit2.ml (100%) rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguate.crit4.ml (100%) rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguate.ml (100%) rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguate.mli (100%) rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguateTypes.ml (100%) rename helm/software/components/{cic_disambiguation => disambiguation}/disambiguateTypes.mli (100%) diff --git a/helm/software/components/METAS/meta.helm-cic_disambiguation.src b/helm/software/components/METAS/meta.helm-cic_disambiguation.src index d2e467aae..6a5d3a38d 100644 --- a/helm/software/components/METAS/meta.helm-cic_disambiguation.src +++ b/helm/software/components/METAS/meta.helm-cic_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-whelp helm-acic_content helm-cic_unification" +requires="helm-whelp helm-acic_content helm-cic_unification helm-disambiguation" version="0.0.1" archive(byte)="cic_disambiguation.cma" archive(native)="cic_disambiguation.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index afe6c3f82..9565ddb29 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -30,6 +30,7 @@ MODULES = \ whelp \ tactics \ acic_procedural \ + disambiguation \ cic_disambiguation \ lexicon \ grafite_engine \ diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index 6ad263c49..9fd0c6639 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,15 +1,6 @@ -disambiguateChoices.cmi: disambiguateTypes.cmi -disambiguate.cmi: disambiguateTypes.cmi -cicDisambiguate.cmi: disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo: disambiguateTypes.cmi -disambiguateTypes.cmx: disambiguateTypes.cmi -disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi -disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi -cicDisambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi \ - cicDisambiguate.cmi -cicDisambiguate.cmx: disambiguateTypes.cmx disambiguate.cmx \ - cicDisambiguate.cmi -number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi +cicDisambiguate.cmo: cicDisambiguate.cmi +cicDisambiguate.cmx: cicDisambiguate.cmi +number_notation.cmo: disambiguateChoices.cmi +number_notation.cmx: disambiguateChoices.cmx diff --git a/helm/software/components/cic_disambiguation/Makefile b/helm/software/components/cic_disambiguation/Makefile index ca4882158..2dc2984de 100644 --- a/helm/software/components/cic_disambiguation/Makefile +++ b/helm/software/components/cic_disambiguation/Makefile @@ -1,10 +1,7 @@ - PACKAGE = cic_disambiguation NOTATIONS = number INTERFACE_FILES = \ - disambiguateTypes.mli \ disambiguateChoices.mli \ - disambiguate.mli \ cicDisambiguate.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ @@ -21,13 +18,3 @@ include ../Makefile.common OCAMLARCHIVEOPTIONS += -linkall -disambiguateTypes.cmi: disambiguateTypes.mli - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLOPT -rectypes $<" - @$(OCAMLOPT) -c -rectypes $< - diff --git a/helm/software/components/disambiguation/Makefile b/helm/software/components/disambiguation/Makefile new file mode 100644 index 000000000..b961efbff --- /dev/null +++ b/helm/software/components/disambiguation/Makefile @@ -0,0 +1,28 @@ +PACKAGE = disambiguation +INTERFACE_FILES = \ + disambiguateTypes.mli \ + disambiguate.mli +IMPLEMENTATION_FILES = \ + $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ + $(patsubst %,%_notation.ml,$(NOTATIONS)) + +all: + +clean: +distclean: + +include ../../Makefile.defs +include ../Makefile.common + +OCAMLARCHIVEOPTIONS += -linkall + +disambiguateTypes.cmi: disambiguateTypes.mli + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< +disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< +disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi + @echo " OCAMLOPT -rectypes $<" + @$(OCAMLOPT) -c -rectypes $< + diff --git a/helm/software/components/cic_disambiguation/disambiguate.crit2.ml b/helm/software/components/disambiguation/disambiguate.crit2.ml similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguate.crit2.ml rename to helm/software/components/disambiguation/disambiguate.crit2.ml diff --git a/helm/software/components/cic_disambiguation/disambiguate.crit4.ml b/helm/software/components/disambiguation/disambiguate.crit4.ml similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguate.crit4.ml rename to helm/software/components/disambiguation/disambiguate.crit4.ml diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguate.ml rename to helm/software/components/disambiguation/disambiguate.ml diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguate.mli rename to helm/software/components/disambiguation/disambiguate.mli diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/disambiguation/disambiguateTypes.ml similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguateTypes.ml rename to helm/software/components/disambiguation/disambiguateTypes.ml diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/disambiguation/disambiguateTypes.mli similarity index 100% rename from helm/software/components/cic_disambiguation/disambiguateTypes.mli rename to helm/software/components/disambiguation/disambiguateTypes.mli diff --git a/helm/software/configure.ac b/helm/software/configure.ac index fd6ca23e1..f542372f8 100644 --- a/helm/software/configure.ac +++ b/helm/software/configure.ac @@ -73,10 +73,12 @@ zip \ # (Matita) findlib requisites FINDLIB_COMREQUIRES="\ +helm-disambiguation \ helm-cic_disambiguation \ helm-grafite \ helm-grafite_engine \ helm-tptp_grafite \ +helm-ng_disambiguation \ helm-grafite_parser \ helm-acic_procedural \ helm-content_pres \ -- 2.39.2