From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Nov 2000 19:50:26 +0000 (+0000)
Subject: Other cleanings in the repository
X-Git-Tag: nogzip~146
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5089686a4d73990a8a284666b388ef3276cec680;p=helm.git

Other cleanings in the repository
---

diff --git a/helm/interface/Makefile b/helm/interface/Makefile
index 14ca2eb19..93e6c97b4 100644
--- 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
index 75156a0c4..000000000
--- 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