X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2Futilities%2Fcreate_environment.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2Futilities%2Fcreate_environment.ml;h=0000000000000000000000000000000000000000;hb=aef659e5893b4bf8c8544d0c54714e10f5b5493a;hp=8a8524d24fdffad4079dbe7d484b334cf8c36266;hpb=64afac782fe3bd83dbc2f9295481362f1edc8e68;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/utilities/create_environment.ml b/helm/software/components/cic_proof_checking/utilities/create_environment.ml
deleted file mode 100644
index 8a8524d24..000000000
--- a/helm/software/components/cic_proof_checking/utilities/create_environment.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-(* Copyright (C) 2004-2005, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-let trust = true
-
-let outfname =
-  match Sys.argv.(1) with
-    | "-help" | "--help" | "-h" | "--h" ->
-          print_endline
-            ("Usage: create_environment <dumpfile> <uri_index>\n" ^
-             "  <dumpfile>   is the file where environment will be dumped\n" ^
-             "  <uri_index>  is the file containing the URIs, one per line,\n" ^
-             "               that will be typechecked. Could be \"-\" for\n" ^
-             "               standard input");
-          flush stdout;
-          exit 0
-    | f -> f
-let _ =
-  CicEnvironment.set_trust (fun _ -> trust);
-  Helm_registry.set "getter.mode" "remote";
-  Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/";
-  Sys.catch_break true;
-  if Sys.file_exists outfname then begin
-    let ic = open_in outfname in
-    CicEnvironment.restore_from_channel ic;
-    close_in ic
-  end
-let urifname =
-  try
-    Sys.argv.(2)
-  with Invalid_argument _ -> "-"
-let ic =
-  match urifname with
-    | "-" -> stdin
-    | fname -> open_in fname
-let _ =
-  try
-    while true do
-(*       try *)
-        let uri = input_line ic in
-        print_endline uri;
-        flush stdout;
-        let uri = UriManager.uri_of_string uri in
-        ignore (CicTypeChecker.typecheck uri)
-(*       with Sys.Break -> () *)
-    done
-  with End_of_file | Sys.Break ->
-    let oc = open_out outfname in
-    CicEnvironment.dump_to_channel oc;
-    close_out oc
-