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 | |
| 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
| -rw-r--r-- | parsing/g_basevernac.ml4 | 8 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
2 files changed, 13 insertions, 3 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index bb6abb70b..e1c219105 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -92,11 +92,15 @@ GEXTEND Gram <:ast< (Locate $id) >> (* For compatibility (now turned into a table) *) + | IDENT "AddPath"; dir = stringarg; IDENT "As"; alias = qualidarg; "." -> + <:ast< (ADDPATH $dir $alias) >> | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >> | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >> | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >> - | IDENT "AddRecPath"; dir = stringarg; "." -> <:ast< (RECADDPATH $dir) >> - + | IDENT "AddRecPath"; dir = stringarg;IDENT "As"; alias=qualidarg; "." -> + <:ast< (RECADDPATH $dir $alias) >> + | IDENT "AddRecPath"; dir = stringarg; "." -> + <:ast< (RECADDPATH $dir) >> | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >> | IDENT "Print"; "Proof"; id = identarg; "." -> <:ast< (PrintOpaqueId $id) >> 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 _ = |