Many cleanings in the repository

diff --git a/helm/interface/ISTRUZIONI b/helm/interface/ISTRUZIONI
deleted file mode 100644 (file)
index fe6c09e..0000000
--- a/helm/interface/ISTRUZIONI
+++ /dev/null
@@ -1,22 +0,0 @@
-==============================
-ISTRUZIONI PER CHI USA LA TCSH
-==============================
-
-Lanciare:
-
- source PER_FARLO_ANDARE_TCSH
-
-Poi far partire altri due xterm.
-Nel primo lanciare:
-
- make start-xaland3
-
-Nel secondo lanciare:
-
- make start-http-getter
-
-Se non funziona significa che ce ne e' gia' uno attivo.
-
-Infini lanciare, dall'ultima shell,
-
- ./mmlinterface.opt.saved

diff --git a/helm/interface/NON_VA b/helm/interface/NON_VA
deleted file mode 100644 (file)
index 3754471..0000000
--- a/helm/interface/NON_VA
+++ /dev/null
@@ -1,29 +0,0 @@
-
- ***********************************************************************
-
-                         A T T E N Z I O N E ! ! !
-
- Quando si usa fix_params.opt, scrivere
-
-       find /really_very_local/helm/PARSER/examples
-
- invece di examples
-
- ***********************************************************************
-
- PROBLEMA NON FIXATO CON fix_params
-
- LA SOLUZIONE E'
-
-
-
-Correggere:
-
- examples/coq/SETS/Powerset_facts/Sets_as_an_algebra/setcover_intro.con.xml
-
-aggiungendo paramMode="POSSIBLE"
-
-Un esempio che altrimenti non funziona e':
-
-examples/coq/SETS/Powerset_Classical_facts/Sets_as_an_algebra/Add_covers.con.xml
-

diff --git a/helm/interface/PER_FARLO_ANDARE b/helm/interface/PER_FARLO_ANDARE
deleted file mode 100644 (file)
index 20fb52a..0000000
--- a/helm/interface/PER_FARLO_ANDARE
+++ /dev/null
@@ -1,2 +0,0 @@
-export LD_LIBRARY_PATH=.:/really_very_local/helm/proveluca/mml-browser/
-export no_proxy=cs.unibo.it

diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH b/helm/interface/PER_FARLO_ANDARE_TCSH
deleted file mode 100644 (file)
index b527fab..0000000
--- a/helm/interface/PER_FARLO_ANDARE_TCSH
+++ /dev/null
@@ -1,4 +0,0 @@
-setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH"
-setenv CLASSPATH "/really_very_local/helm/java/xalan_1_1/xalan.jar:/really_very_local/helm/java/xalan_1_1/xerces.jar:."
-setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH"
-setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/"

diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH_D01 b/helm/interface/PER_FARLO_ANDARE_TCSH_D01
deleted file mode 100644 (file)
index 208f00a..0000000
--- a/helm/interface/PER_FARLO_ANDARE_TCSH_D01
+++ /dev/null
@@ -1,4 +0,0 @@
-setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH"
-setenv CLASSPATH "/really_very_local/helm/java/xalan_1_2_D01/xalan.jar:/really_very_local/helm/java/xalan_1_2_D01/xerces.jar:."
-setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH"
-setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/"

diff --git a/helm/interface/cicXPath.prima_degli_identificatori.ml b/helm/interface/cicXPath.prima_degli_identificatori.ml
deleted file mode 100644 (file)
index 8a69d1a..0000000
--- a/helm/interface/cicXPath.prima_degli_identificatori.ml
+++ /dev/null
@@ -1,102 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 11/04/2000                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* functions to parse an XPath to retrieve the annotation *)
-
-exception WrongXPath of string;;
-
-let rec get_annotation_of_inductiveFun f xpath =
- let module C = Cic in
-  match (xpath,f) with
-     1::tl,(_,_,ty,_) -> get_annotation_of_term ty tl
-   | 2::tl,(_,_,_,te) -> get_annotation_of_term te tl
-   | l,_ ->
-      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
-
-and get_annotation_of_coinductiveFun f xpath =
- let module C = Cic in
-  match (xpath,f) with
-     1::tl,(_,ty,_) -> get_annotation_of_term ty tl
-   | 2::tl,(_,_,te) -> get_annotation_of_term te tl
-   | l,_ ->
-      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
-
-and get_annotation_of_inductiveType ty xpath =
- let module C = Cic in
-  match (xpath,ty) with
-     1::tl,(_,_,arity,_) -> get_annotation_of_term arity tl
-   | n::tl,(_,_,_,cons) when n <= List.length cons + 1 ->
-      let (_,ty,_) = List.nth cons (n-2) in
-       get_annotation_of_term ty tl
-   | l,_ ->
-      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
-
-and get_annotation_of_term term xpath =
- let module C = Cic in
-  match (xpath,term) with
-     [],C.ARel (_,ann,_,_) -> ann
-   | [],C.AVar (_,ann,_) -> ann
-   | [],C.AMeta (_,ann,_) -> ann
-   | [],C.ASort (_,ann,_) -> ann
-   | [],C.AImplicit (_,ann) -> ann
-   | [],C.ACast (_,ann,_,_) -> ann
-   | 1::tl,C.ACast (_,_,te,_) -> get_annotation_of_term te tl
-   | 2::tl,C.ACast (_,_,_,ty) -> get_annotation_of_term ty tl
-   | [],C.AProd (_,ann,_,_,_) -> ann
-   | 1::tl,C.AProd (_,_,_,so,_) -> get_annotation_of_term so tl
-   | 2::tl,C.AProd (_,_,_,_,ta) -> get_annotation_of_term ta tl
-   | [],C.ALambda (_,ann,_,_,_) -> ann
-   | 1::tl,C.ALambda (_,_,_,so,_) -> get_annotation_of_term so tl
-   | 2::tl,C.ALambda (_,_,_,_,ta) -> get_annotation_of_term ta tl
-   | [],C.AAppl (_,ann,_) -> ann
-   | n::tl,C.AAppl (_,_,l) when n <= List.length l ->
-      get_annotation_of_term (List.nth l (n-1)) tl
-   | [],C.AConst (_,ann,_,_) -> ann
-   | [],C.AAbst (_,ann,_) -> ann
-   | [],C.AMutInd (_,ann,_,_,_) -> ann
-   | [],C.AMutConstruct (_,ann,_,_,_,_) -> ann
-   | [],C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
-   | 1::tl,C.AMutCase (_,_,_,_,_,outt,_,_) -> get_annotation_of_term outt tl
-   | 2::tl,C.AMutCase (_,_,_,_,_,_,te,_) -> get_annotation_of_term te tl
-   | n::tl,C.AMutCase (_,_,_,_,_,_,_,pl) when n <= List.length pl ->
-      get_annotation_of_term (List.nth pl (n-1)) tl
-   | [],C.AFix (_,ann,_,_) -> ann
-   | n::tl,C.AFix (_,_,_,fl) when n <= List.length fl ->
-      get_annotation_of_inductiveFun (List.nth fl (n-1)) tl
-   | [],C.ACoFix (_,ann,_,_) -> ann
-   | n::tl,C.ACoFix (_,_,_,fl) when n <= List.length fl ->
-      get_annotation_of_coinductiveFun (List.nth fl (n-1)) tl
-   | l,_ ->
-      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
-;;
-
-let get_annotation (annobj,_) xpath =
- let module C = Cic in
-  match (xpath,annobj) with
-     [],C.ADefinition (_,ann,_,_,_,_) -> ann
-   | 1::tl,C.ADefinition (_,_,_,bo,_,_) -> get_annotation_of_term bo tl
-   | 2::tl,C.ADefinition (_,_,_,_,ty,_) -> get_annotation_of_term ty tl
-   | [],C.AAxiom (_,ann,_,_,_) -> ann
-   | 1::tl,C.AAxiom (_,_,_,ty,_) -> get_annotation_of_term ty tl
-   | [],C.AVariable (_,ann,_,_) -> ann
-   | 1::tl,C.AVariable (_,_,_,ty) -> get_annotation_of_term ty tl
-   | [],C.ACurrentProof (_,ann,_,_,_,_) -> ann
-   | n::tl,C.ACurrentProof (_,ann,_,conjs,_,_) when n <= List.length conjs ->
-      get_annotation_of_term (snd (List.nth conjs (n-1))) tl
-   | n::tl,C.ACurrentProof (_,ann,_,conjs,bo,_) when n = List.length conjs + 1 ->
-      get_annotation_of_term bo tl
-   | n::tl,C.ACurrentProof (_,ann,_,conjs,_,ty) when n = List.length conjs + 2 ->
-      get_annotation_of_term ty tl
-   | [],C.AInductiveDefinition (_,ann,_,_,_) -> ann
-   | n::tl,C.AInductiveDefinition (_,_,tys,_,_) when n <= List.length tys ->
-      get_annotation_of_inductiveType (List.nth tys (n-1)) tl
-   | l,_ ->
-      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
-;;

diff --git a/helm/interface/gmon.out b/helm/interface/gmon.out
deleted file mode 100644 (file)
index c48b840..0000000
Binary files a/helm/interface/gmon.out and /dev/null differ

diff --git a/helm/interface/latinize.pl b/helm/interface/latinize.pl
deleted file mode 100755 (executable)
index 7fa6787..0000000
--- a/helm/interface/latinize.pl
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/perl
-
-while(<STDIN>)
-{
-  s/&#8594;/->/g;
-  s/&#8658;/=>/g;
-  s/&#955;/\\/g;
-  s/&#928;/||/g;
-  print;
-}

diff --git a/helm/interface/mml.dtd b/helm/interface/mml.dtd
deleted file mode 100644 (file)
index 10ce5cb..0000000
--- a/helm/interface/mml.dtd
+++ /dev/null
@@ -1,55 +0,0 @@
-<?xml encoding="ISO-8859-1"?>
-
-<!-- CSC: mio DTD semplificatissimo per la parte presentation di MML -->
-
-<!-- I seguenti presentation elements sono stati tralasciati ;-)
-mspace
-ms
-<mchar>
-<ms>
-mfrac
-msqrt
-mroot
-mstyle
-merror
-mpadded
-mphantom
-msub
-msup
-msubsup
-munder
-mover
-munderover
-mmultiscripts
-mtable
-mtr
-mtd
-maligngroup
-malignmark
-maction
--->
-
-<!-- Dei seguenti elementi, invece, vengono tralasciati quasi tutti gli
-     attributi
-&ApplyFunction;
--->
-
-<!ENTITY % Presentation '(mi|mo|mn|mtext|mrow|mfenced)*'>
-
-<!ELEMENT math %Presentation;>
-
-<!ELEMENT mi (#PCDATA)>
-
-<!ELEMENT mo (#PCDATA)>
-
-<!ELEMENT mn (#PCDATA)>
-
-<!ELEMENT mtext (#PCDATA)>
-
-<!ELEMENT mrow %Presentation;>
-
-<!ELEMENT mfenced %Presentation;>
-<!ATTLIST mfenced
-          open       CDATA #IMPLIED
-          close      CDATA #IMPLIED
-          separators CDATA #IMPLIED>

diff --git a/helm/interface/mml.ml b/helm/interface/mml.ml
deleted file mode 100644 (file)
index 88c2813..0000000
--- a/helm/interface/mml.ml
+++ /dev/null
@@ -1,11 +0,0 @@
-type expr =
-   Null
- | Mi of string
- | Mo of string
- | Mn of string
- | Mtext of string
- | Mrow of expr list
- | Mfenced of string * string * string * expr list (* open, close, separators *)
-type fragment =
- Math of expr list
-;;

diff --git a/helm/interface/mmlinterface.opt.saved b/helm/interface/mmlinterface.opt.saved
deleted file mode 100755 (executable)
index cb5708a..0000000
Binary files a/helm/interface/mmlinterface.opt.saved and /dev/null differ