Other cleanings in the repository

diff --git a/helm/interface/Makefile b/helm/interface/Makefile
index 14ca2eb19e90246b89ffcdb743067424d64f2619..93e6c97b41559ad9e614b5f3b8249ee36904cc27 100644 (file)
--- a/helm/interface/Makefile
+++ b/helm/interface/Makefile
@@ -29,7 +29,7 @@ DEPOBJS = experiment.ml cicCache.ml cicCache.mli cicPp.ml cicPp.mli \
           theoryParser.ml theoryParser2.ml theoryPp.ml theoryTypeChecker.ml \
           cicCooking.ml cicCooking.mli cicFindParameters.ml theoryCache.ml \
           fix_params.ml cic2Xml.ml xml.ml uriManager.ml uriManager.mli \
-          cicSubstitution.ml cicSubstitution.mli mml.ml \
+          cicSubstitution.ml cicSubstitution.mli \
           mmlinterface.ml configuration.ml \
           xsltProcessor.ml deannotate.ml cicXPath.ml pxpUriResolver.ml \
           annotationParser.ml annotationParser2.ml annotation2Xml.ml \
@@ -40,7 +40,7 @@ MMLINTERFACEOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \
                    cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \
                    cicSubstitution.cmo annotationParser2.cmo \
                    annotationParser.cmo cicCache.cmo cicCooking.cmo cicPp.cmo \
-                   cicReduction.cmo cicTypeChecker.cmo mml.cmo \
+                   cicReduction.cmo cicTypeChecker.cmo \
                    xml.cmo \
                    xsltProcessor.cmo cic2Xml.cmo annotation2Xml.cmo \
                    cicXPath.cmo theory.cmo theoryParser2.cmo theoryParser.cmo \
@@ -53,7 +53,7 @@ MMLINTERFACEOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \
                       deannotate.cmx cicSubstitution.cmx annotationParser2.cmx \
                       annotationParser.cmx cicCache.cmx \
                       cicCooking.cmx cicPp.cmx cicReduction.cmx \
-                      cicTypeChecker.cmx mml.cmx \
+                      cicTypeChecker.cmx \
                       xml.cmx xsltProcessor.cmx \
                       cic2Xml.cmx annotation2Xml.cmx cicXPath.cmx \
                       theory.cmx theoryParser2.cmx theoryParser.cmx \

diff --git a/helm/interface/mkindex.sh b/helm/interface/mkindex.sh
deleted file mode 100755 (executable)
index 75156a0..0000000
--- a/helm/interface/mkindex.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/bin/bash
-
-echo `find . -name "*.xml"` | ~/HELM/interface/uris_of_filenames.pl > index.txt