diff options
| -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 bb6abb70bd..e1c2191057 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 4277921477..54fcda3059 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 _ = |