From 07a27a457b19ccaaf318321502e7330d5507fbf2 Mon Sep 17 00:00:00 2001
From: sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 29 Nov 2000 13:56:52 +0000
Subject: 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
---
 parsing/g_basevernac.ml4  | 8 ++++++--
 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 _ =
-- 
cgit v1.2.3