diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 13:56:52 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 13:56:52 +0000 |
| commit | 07a27a457b19ccaaf318321502e7330d5507fbf2 (patch) | |
| tree | 7b85af4a903f6683d3eab117411a0572ecd5fa0b /toplevel | |
| parent | 3401245dbadb9e6e7aedc03c64afc3fbe7d190d1 (diff) | |
Now AddRecPath and AddPath can be used with an As option to specify the
Coq dir path.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1025 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 427792147..54fcda305 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -170,6 +170,9 @@ let _ = if alias = "" then error ("Cannot map "^dir^" to a root of Coq library"); (fun () -> add_path dir [alias]) + | [VARG_STRING dir ; VARG_QUALID alias] -> + let aliasdir,aliasname = repr_qualid alias in + (fun () -> add_path dir (aliasdir@[aliasname])) | _ -> bad_vernac_args "ADDPATH") (* For compatibility *) @@ -187,6 +190,9 @@ let _ = if alias = "" then error ("Cannot map "^dir^" to a root of Coq library"); (fun () -> rec_add_path dir [alias]) + | [VARG_STRING dir ; VARG_QUALID alias] -> + let aliasdir,aliasname = repr_qualid alias in + (fun () -> rec_add_path dir (aliasdir@[aliasname])) | _ -> bad_vernac_args "RECADDPATH") (* For compatibility *) @@ -294,7 +300,7 @@ let _ = let s = string_of_id id in let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in - fun () -> Lib.start_module (lpe.relative_subdir @ [s]) + fun () -> Lib.start_module (lpe.coq_dirpath @ [s]) | _ -> bad_vernac_args "BeginModule") let _ = |