diff options
| author | filliatr | 1999-12-10 08:57:01 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-10 08:57:01 +0000 |
| commit | 85bd945e22abc31fec8f89da1779d94027323e91 (patch) | |
| tree | 356cfc0aa9a5f6b2328b05a4509d76bbd89a73e7 /toplevel | |
| parent | baa3e16836c3f0daf24ba47aadbdee525762d6ec (diff) | |
debug discharge et inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 14 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 9 insertions, 11 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5d968321a7..474b247a68 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -58,13 +58,17 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft let init_load_path () = (* default load path; only if COQLIB is defined *) let coqlib = getenv_else "COQLIB" Coq_config.coqlib in - if coqlib <> "" then - List.iter - (fun s -> add_include (Filename.concat coqlib s)) - ("states" :: + let coqtop = getenv_else "COQTOP" Coq_config.coqtop in + if coqlib = coqtop then + (* local installation *) + List.iter + (fun s -> add_include (Filename.concat coqtop s)) + ("states" :: "dev" :: (List.map (fun s -> Filename.concat "theories" (hm2 s)) - Coq_config.theories_dirs)); + Coq_config.theories_dirs)) + else + add_include coqlib; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_include camlp4; add_include "."; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 17127518c0..e1396fb3a9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -236,12 +236,6 @@ let _ = (*** let _ = - add "ResetAfter" - (function - | [VARG_IDENTIFIER id] -> (fun () -> reset_keeping_name id) - | _ -> bad_vernac_args "ResetAfter") - -let _ = add "ResetInitial" (function | [] -> (fun () -> reset_initial ()) |