aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorbarras2001-05-23 15:13:07 +0000
committerbarras2001-05-23 15:13:07 +0000
commitdc2e676c9cdedea43805c21a4b3203832a985f95 (patch)
tree849760ef13d1460d603ce9436c244922e13a6080 /dev/base_include
parenta023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff)
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include26
1 files changed, 1 insertions, 25 deletions
diff --git a/dev/base_include b/dev/base_include
index 2515cabd39..8ef9fc5baf 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -1,30 +1,6 @@
(* File to include to get some Coq facilities under the ocaml toplevel.
- This file is loaded by include.ml *)
-
-(* We only assume that the variable COQTOP is set *)
-let src_dir =
- let coqtop = try Sys.getenv "COQTOP" with Not_found -> "." in
- let coqtop =
- if Sys.file_exists coqtop then
- coqtop
- else begin
- print_endline ("Cannot find the sources in "^coqtop);
- print_string "Where are they ? ";
- read_line ()
- end
- in
- let add_dir dl =
- Topdirs.dir_directory (List.fold_left Filename.concat coqtop dl)
- in
- List.iter add_dir
- [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
- [ "pretyping" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ];
- [ "toplevel" ] ];
- coqtop
-;;
-(* Now Coq_config.cmi is accessible *)
-Topdirs.dir_directory Coq_config.camlp4lib;;
+ This file is loaded by include *)
#use "top_printers.ml";;