Makefile.common.in and .depend backtracked to my last commit (before the

ones of Ferruccio) and then modified. Dependencies between a file and a
library are now handled correctly.

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
new file mode 100644 (file)
index 0000000..fa167f5
--- /dev/null
+++ b/helm/gTopLevel/.depend
@@ -0,0 +1,52 @@
+xml2Gdome.cmo: xml2Gdome.cmi 
+xml2Gdome.cmx: xml2Gdome.cmi 
+proofEngine.cmo: proofEngine.cmi 
+proofEngine.cmx: proofEngine.cmi 
+doubleTypeInference.cmo: doubleTypeInference.cmi 
+doubleTypeInference.cmx: doubleTypeInference.cmi 
+cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi 
+cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi 
+cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi 
+cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi 
+cic2Xml.cmi: cic2acic.cmi 
+logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
+logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi 
+sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi 
+sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi 
+mQueryLevels.cmo: mQueryLevels.cmi 
+mQueryLevels.cmx: mQueryLevels.cmi 
+mQueryLevels2.cmi: mQueryGenerator.cmi 
+mQueryLevels2.cmo: mQueryLevels2.cmi 
+mQueryLevels2.cmx: mQueryLevels2.cmi 
+mQueryGenerator.cmo: mQueryGenerator.cmi 
+mQueryGenerator.cmx: mQueryGenerator.cmi 
+misc.cmo: misc.cmi 
+misc.cmx: misc.cmi 
+disambiguate.cmo: mQueryGenerator.cmi misc.cmi disambiguate.cmi 
+disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi 
+termEditor.cmo: disambiguate.cmi termEditor.cmi 
+termEditor.cmx: disambiguate.cmx termEditor.cmi 
+termEditor.cmi: disambiguate.cmi 
+applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \
+    applyStylesheets.cmi 
+applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \
+    applyStylesheets.cmi 
+applyStylesheets.cmi: cic2acic.cmi 
+termViewer.cmo: applyStylesheets.cmi cic2acic.cmi logicalOperations.cmi \
+    misc.cmi termViewer.cmi 
+termViewer.cmx: applyStylesheets.cmx cic2acic.cmx logicalOperations.cmx \
+    misc.cmx termViewer.cmi 
+termViewer.cmi: cic2acic.cmi 
+invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \
+    termViewer.cmi invokeTactics.cmi 
+invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \
+    termViewer.cmx invokeTactics.cmi 
+invokeTactics.cmi: termEditor.cmi termViewer.cmi 
+gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \
+    invokeTactics.cmi logicalOperations.cmi mQueryGenerator.cmi \
+    mQueryLevels.cmi mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi \
+    termEditor.cmi termViewer.cmi 
+gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \
+    invokeTactics.cmx logicalOperations.cmx mQueryGenerator.cmx \
+    mQueryLevels.cmx mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx \
+    termEditor.cmx termViewer.cmx 

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 5f630f23c7f05187b48fab150a397304fad33b88..7822b1ace7d0fa5accc5b68359a0540551c605f7 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -4,7 +4,6 @@ REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
            helm-mathql_interpreter
 PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
-OCAMLDEPOPTIONS = $(shell ocamlfind query -recursive -predicates "$(PREDICATES)" -i-format $(REQUIRES))
 OCAMLFIND = ocamlfind
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS)
 OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
@@ -34,7 +33,7 @@ TOPLEVELOBJS = \
         gTopLevel.cmo
 
 depend:
-       $(OCAMLDEP) $(OCAMLDEPOPTIONS) $(DEPOBJS) > .depend
+       $(OCAMLDEP) $(DEPOBJS) > .depend
 
 gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES)
        $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS)
@@ -43,13 +42,16 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
        $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx)
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx
-.ml.cmo: $(LIBRARIES)
+.ml.cmo:
        $(OCAMLC) -c $<
-.mli.cmi: $(LIBRARIES)
+.mli.cmi:
        $(OCAMLC) -c $<
-.ml.cmx: $(LIBRARIES_OPT)
+.ml.cmx:
        $(OCAMLOPT) -c $<
 
+$(TOPLEVELOBJS): $(LIBRARIES)
+$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT)
+
 clean:
        rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt
 

diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in
index 519b2ea9a7500e3f780af088b024d72f29168e37..42015d622c7869c5eb815da053fcef4f3038af49 100644 (file)
--- a/helm/ocaml/Makefile.common.in
+++ b/helm/ocaml/Makefile.common.in
@@ -19,7 +19,7 @@ OCAMLYACC = ocamlyacc
 
 LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-OCAMLDEPOPTIONS = $(shell ocamlfind query -recursive -predicates "$(PREDICATES)" -i-format $(REQUIRES))
+
 
 ARCHIVE = $(PACKAGE).cma
 ARCHIVE_OPT = $(PACKAGE).cmxa
@@ -38,14 +38,14 @@ all: $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
 opt: $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
 
 depend: $(DEPEND_FILES)
-       $(OCAMLDEP) $(OCAMLDEPOPTIONS) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
+       $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly
-.ml.cmo: $(LIBRARIES)
+.ml.cmo:
        $(OCAMLC) -c $<
-.mli.cmi: $(LIBRARIES)
+.mli.cmi:
        $(OCAMLC) -c $<
-.ml.cmx: $(LIBRARIES_OPT)
+.ml.cmx:
        $(OCAMLOPT) -c $<
 .mly.ml:
        $(OCAMLYACC) $<
@@ -54,6 +54,9 @@ depend: $(DEPEND_FILES)
 .mll.ml:
        $(OCAMLLEX) $<
 
+$(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES)
+$(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT)
+
 clean:
        rm -f *.cm[ioax] *.cmxa *.o *.a $(EXTRA_OBJECTS_TO_CLEAN)
 

diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend
new file mode 100644 (file)
index 0000000..591cea8
--- /dev/null
+++ b/helm/ocaml/cic/.depend
@@ -0,0 +1,12 @@
+deannotate.cmi: cic.cmo 
+cicParser3.cmi: cic.cmo 
+cicParser2.cmi: cic.cmo cicParser3.cmi 
+cicParser.cmi: cic.cmo 
+deannotate.cmo: cic.cmo deannotate.cmi 
+deannotate.cmx: cic.cmx deannotate.cmi 
+cicParser3.cmo: cic.cmo cicParser3.cmi 
+cicParser3.cmx: cic.cmx cicParser3.cmi 
+cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi 
+cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi 
+cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi 
+cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi 

diff --git a/helm/ocaml/cic_annotations/.depend b/helm/ocaml/cic_annotations/.depend
new file mode 100644 (file)
index 0000000..2c30fa7
--- /dev/null
+++ b/helm/ocaml/cic_annotations/.depend
@@ -0,0 +1,8 @@
+cicXPath.cmo: cicXPath.cmi 
+cicXPath.cmx: cicXPath.cmi 
+cicAnnotation2Xml.cmo: cicXPath.cmi cicAnnotation2Xml.cmi 
+cicAnnotation2Xml.cmx: cicXPath.cmx cicAnnotation2Xml.cmi 
+cicAnnotationParser2.cmo: cicAnnotationParser2.cmi 
+cicAnnotationParser2.cmx: cicAnnotationParser2.cmi 
+cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi 
+cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi 

diff --git a/helm/ocaml/cic_annotations_cache/.depend b/helm/ocaml/cic_annotations_cache/.depend
new file mode 100644 (file)
index 0000000..06775e1
--- /dev/null
+++ b/helm/ocaml/cic_annotations_cache/.depend
@@ -0,0 +1,2 @@
+cicCache.cmo: cicCache.cmi 
+cicCache.cmx: cicCache.cmi 

diff --git a/helm/ocaml/cic_cache/.depend b/helm/ocaml/cic_cache/.depend
new file mode 100644 (file)
index 0000000..06775e1
--- /dev/null
+++ b/helm/ocaml/cic_cache/.depend
@@ -0,0 +1,2 @@
+cicCache.cmo: cicCache.cmi 
+cicCache.cmx: cicCache.cmi 

diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend
new file mode 100644 (file)
index 0000000..c1319a6
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/.depend
@@ -0,0 +1,22 @@
+logger.cmo: logger.cmi 
+logger.cmx: logger.cmi 
+cicEnvironment.cmo: logger.cmi cicEnvironment.cmi 
+cicEnvironment.cmx: logger.cmx cicEnvironment.cmi 
+cicPp.cmo: cicEnvironment.cmi cicPp.cmi 
+cicPp.cmx: cicEnvironment.cmx cicPp.cmi 
+cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi 
+cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi 
+cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi 
+cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi 
+cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \
+    cicReductionNaif.cmi 
+cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \
+    cicReductionNaif.cmi 
+cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \
+    cicReduction.cmi 
+cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \
+    cicReduction.cmi 
+cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \
+    cicSubstitution.cmi logger.cmi cicTypeChecker.cmi 
+cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \
+    cicSubstitution.cmx logger.cmx cicTypeChecker.cmi 

diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend
new file mode 100644 (file)
index 0000000..d7aabf8
--- /dev/null
+++ b/helm/ocaml/cic_textual_parser/.depend
@@ -0,0 +1,10 @@
+cicTextualParser.cmi: cicTextualParser0.cmo 
+cicTextualParserContext.cmi: cicTextualParser.cmi cicTextualParser0.cmo 
+cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi 
+cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.cmi 
+cicTextualParserContext.cmo: cicTextualParser.cmi cicTextualParser0.cmo \
+    cicTextualParserContext.cmi 
+cicTextualParserContext.cmx: cicTextualParser.cmx cicTextualParser0.cmx \
+    cicTextualParserContext.cmi 
+cicTextualLexer.cmo: cicTextualParser.cmi 
+cicTextualLexer.cmx: cicTextualParser.cmx 

diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend
new file mode 100644 (file)
index 0000000..d22689d
--- /dev/null
+++ b/helm/ocaml/cic_unification/.depend
@@ -0,0 +1,5 @@
+cicRefine.cmi: cicUnification.cmi 
+cicUnification.cmo: cicUnification.cmi 
+cicUnification.cmx: cicUnification.cmi 
+cicRefine.cmo: cicUnification.cmi cicRefine.cmi 
+cicRefine.cmx: cicUnification.cmx cicRefine.cmi 

diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend
new file mode 100644 (file)
index 0000000..2013e9b
--- /dev/null
+++ b/helm/ocaml/getter/.depend
@@ -0,0 +1,6 @@
+configuration.cmo: configuration.cmi 
+configuration.cmx: configuration.cmi 
+clientHTTP.cmo: configuration.cmi clientHTTP.cmi 
+clientHTTP.cmx: configuration.cmx clientHTTP.cmi 
+getter.cmo: clientHTTP.cmi configuration.cmi getter.cmi 
+getter.cmx: clientHTTP.cmx configuration.cmx getter.cmi 

diff --git a/helm/ocaml/pxp/.depend b/helm/ocaml/pxp/.depend
new file mode 100644 (file)
index 0000000..c2a1a4b
--- /dev/null
+++ b/helm/ocaml/pxp/.depend
@@ -0,0 +1,2 @@
+pxpUrlResolver.cmo: pxpUrlResolver.cmi 
+pxpUrlResolver.cmx: pxpUrlResolver.cmi 

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
new file mode 100644 (file)
index 0000000..e6dc05b
--- /dev/null
+++ b/helm/ocaml/tactics/.depend
@@ -0,0 +1,77 @@
+proofEngineHelpers.cmi: proofEngineTypes.cmo 
+tacticals.cmi: proofEngineTypes.cmo 
+reductionTactics.cmi: proofEngineTypes.cmo 
+proofEngineStructuralRules.cmi: proofEngineTypes.cmo 
+primitiveTactics.cmi: proofEngineTypes.cmo 
+variousTactics.cmi: proofEngineTypes.cmo 
+introductionTactics.cmi: proofEngineTypes.cmo 
+eliminationTactics.cmi: proofEngineTypes.cmo 
+negationTactics.cmi: proofEngineTypes.cmo 
+equalityTactics.cmi: proofEngineTypes.cmo 
+discriminationTactics.cmi: proofEngineTypes.cmo 
+ring.cmi: proofEngineTypes.cmo 
+fourierR.cmi: proofEngineTypes.cmo 
+proofEngineReduction.cmo: proofEngineReduction.cmi 
+proofEngineReduction.cmx: proofEngineReduction.cmi 
+proofEngineHelpers.cmo: proofEngineHelpers.cmi 
+proofEngineHelpers.cmx: proofEngineHelpers.cmi 
+fourier.cmo: fourier.cmi 
+fourier.cmx: fourier.cmi 
+tacticals.cmo: proofEngineTypes.cmo tacticals.cmi 
+tacticals.cmx: proofEngineTypes.cmx tacticals.cmi 
+reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi 
+reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi 
+proofEngineStructuralRules.cmo: proofEngineTypes.cmo \
+    proofEngineStructuralRules.cmi 
+proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmi 
+primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \
+    proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \
+    primitiveTactics.cmi 
+primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
+    proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
+    primitiveTactics.cmi 
+variousTactics.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \
+    proofEngineReduction.cmi proofEngineTypes.cmo tacticals.cmi \
+    variousTactics.cmi 
+variousTactics.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \
+    proofEngineReduction.cmx proofEngineTypes.cmx tacticals.cmx \
+    variousTactics.cmi 
+introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \
+    introductionTactics.cmi 
+introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \
+    introductionTactics.cmi 
+eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \
+    tacticals.cmi eliminationTactics.cmi 
+eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \
+    tacticals.cmx eliminationTactics.cmi 
+negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \
+    proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi 
+negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \
+    proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi 
+equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \
+    proofEngineHelpers.cmi proofEngineReduction.cmi \
+    proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \
+    tacticals.cmi equalityTactics.cmi 
+equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \
+    proofEngineHelpers.cmx proofEngineReduction.cmx \
+    proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \
+    tacticals.cmx equalityTactics.cmi 
+discriminationTactics.cmo: eliminationTactics.cmi equalityTactics.cmi \
+    introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmo \
+    tacticals.cmi discriminationTactics.cmi 
+discriminationTactics.cmx: eliminationTactics.cmx equalityTactics.cmx \
+    introductionTactics.cmx primitiveTactics.cmx proofEngineTypes.cmx \
+    tacticals.cmx discriminationTactics.cmi 
+ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \
+    proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \
+    ring.cmi 
+ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \
+    proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \
+    ring.cmi 
+fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \
+    proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \
+    tacticals.cmi fourierR.cmi 
+fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \
+    proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \
+    tacticals.cmx fourierR.cmi 

diff --git a/helm/ocaml/urimanager/.depend b/helm/ocaml/urimanager/.depend
new file mode 100644 (file)
index 0000000..4821484
--- /dev/null
+++ b/helm/ocaml/urimanager/.depend
@@ -0,0 +1,2 @@
+uriManager.cmo: uriManager.cmi 
+uriManager.cmx: uriManager.cmi 

diff --git a/helm/ocaml/xml/.depend b/helm/ocaml/xml/.depend
new file mode 100644 (file)
index 0000000..bc6941b
--- /dev/null
+++ b/helm/ocaml/xml/.depend
@@ -0,0 +1,2 @@
+xml.cmo: xml.cmi 
+xml.cmx: xml.cmi