Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 9 insertions, 16 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3d1ce4533..f9a0fdc3c 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -135,7 +135,7 @@ let interp_qualid p =
     | [] -> anomaly "interp_qualid: empty qualified identifier"
     | l -> 
 	let p, r = list_chop (List.length l -1) (List.map outnvar l) in
-	make_qualid p (List.hd r)
+	make_qualid (make_dirpath p) (List.hd r)
 
 let maybe_variable = function
   | [Nvar (_,s)] -> Some s
@@ -255,7 +255,7 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],s -> ast_to_var env vars loc s
+      | d,s when is_empty_dirpath d -> ast_to_var env vars loc s
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference or a syntactic definition? *)
@@ -573,7 +573,7 @@ let adjust_qualid env loc ast qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],id -> ast_of_var env ast id
+      | d,id when is_empty_dirpath d -> ast_of_var env ast id
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference or a syntactic definition? *)
@@ -592,7 +592,7 @@ let ast_adjust_consts sigma =
     | Nmeta (loc, s) as ast -> ast
     | Nvar (loc, id) as ast ->
         if Idset.mem id env then ast
-        else adjust_qualid env loc ast (make_qualid [] id)
+        else adjust_qualid env loc ast (make_short_qualid id)
     | Node (loc, "QUALID", p) as ast ->
 	adjust_qualid env loc ast (interp_qualid p)
     | Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f98746a25..af4df3b6f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -149,12 +149,6 @@ GEXTEND Gram
           <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
       ] ]
   ;
-  gallina_ext:
-      [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
-        ":="; c = constrarg ->
-          <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
-      ] ]
-  ;
   END
 
 (* Gallina inductive declarations *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5f804f3f2..7baad745a 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -350,8 +350,8 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (_,Lib.OpenedSection (id,_)) -> 
-        [< 'sTR " >>>>>>> Section "; pr_id id; 'fNL >]
+    | (sp,Lib.OpenedSection (dir,_)) -> 
+        [< 'sTR " >>>>>>> Section "; pr_id (basename sp); 'fNL >]
     | (sp,Lib.ClosedSection _) -> 
         [< 'sTR " >>>>>>> Closed Section "; pr_id (basename sp); 'fNL >]
     | (_,Lib.Module dir) ->
@@ -391,8 +391,7 @@ let read_sec_context qid =
     try Nametab.locate_section qid
     with Not_found -> error "Unknown section" in
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection (_,_)) as hd)::rest ->
-	let dir' = make_dirpath (wd_of_sp sp) in
+    | ((sp,Lib.OpenedSection (dir',_)) as hd)::rest ->
         if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | ((sp,Lib.ClosedSection (_,_,ctxt)) as hd)::rest ->
         error "Cannot print the contents of a closed section"
@@ -440,7 +439,7 @@ let print_name qid =
   with Not_found -> 
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
-    if dir <> [] then raise Not_found;
+    if not (is_empty_dirpath dir) then raise Not_found;
     let (c,typ) = Global.lookup_named str in 
     [< print_named_decl (str,c,typ) >]
   with Not_found ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index d84c5e952..4a686a17e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -107,7 +107,7 @@ let ast_of_ref = function
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
-  let args = List.map nvar (dir@[s]) in
+  let args = List.map nvar ((repr_dirpath dir)@[s]) in
   ope ("QUALID", args)
 
 (**********************************************************************)