Modules dans COQ\!\!\!\!

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

9 files changed, 65 insertions, 58 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 92f6f285f8..a0620d4ba2 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -7,6 +7,7 @@ open Util;;
 open Ast;;
 open Term;;
 open Pp;;
+open Libnames;;
 open Libobject;;
 open Library;;
 open Vernacinterp;;
@@ -258,9 +259,8 @@ let filter_by_module_from_varg_list l =
 
 let add_search (global_reference:global_reference) assumptions cstr =
   try 
-    let env = Global.env() in
   let id_string =
-    string_of_qualid (Nametab.shortest_qualid_of_global env 
+    string_of_qualid (Nametab.shortest_qualid_of_global None 
 			global_reference) in
   let ast = 
     try
@@ -321,15 +321,13 @@ and ntyp = nf_betaiota typ in
 
 (* The following function is copied from globpr in env/printer.ml *)
 let globcv x =
-  let env = Global.env() in 
     match x with
       | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
-	  let env = Global.env() in
 	    convert_qualid
-	      (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi)))
+	      (Nametab.shortest_qualid_of_global None (IndRef(sp,tyi)))
       | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
 	  convert_qualid
-            (Nametab.shortest_qualid_of_global env
+            (Nametab.shortest_qualid_of_global None
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
@@ -412,20 +410,20 @@ let inspect n =
       (fun a ->
 	 try
            (match a with
-             	sp, Lib.Leaf lobj ->
-		  (match sp, object_tag lobj with
-                       _, "VARIABLE" ->
+             	oname, Lib.Leaf lobj ->
+		  (match oname, object_tag lobj with
+                       (sp,_), "VARIABLE" ->
 			 let ((_, _, v), _) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
-		     | sp, ("CONSTANT"|"PARAMETER") ->
-			 let {const_type=typ} = Global.lookup_constant sp in
+		     | (sp,kn), ("CONSTANT"|"PARAMETER") ->
+			 let {const_type=typ} = Global.lookup_constant kn in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
-		     | sp, "MUTUALINDUCTIVE" ->
+		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
 			   (Pretyping.understand Evd.empty (Global.env())
-			      (RRef(dummy_loc, IndRef(sp,0))))
+			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
-				      (string_of_id (basename sp))))
+				      (string_of_id (basename (fst oname)))))
               | _ -> failwith "unexpected value")
 	 with e -> ())
       l;
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index c5611f985a..2345ff4719 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -1,6 +1,7 @@
 (* A copy of pre V7 ast *)
 
 open Names
+open Libnames
 
 type loc = int * int
 
@@ -17,7 +18,7 @@ type t =
 let section_path sl =
   match List.rev sl with
     | s::pa ->
-	make_path
+	Libnames.encode_kn
 	  (make_dirpath (List.map id_of_string pa))
 	  (id_of_string s)
     | [] -> invalid_arg "section_path"
@@ -55,7 +56,7 @@ let rec ast_to_ct = function
   | Coqast.Id (loc,a) -> Id (loc,a)
   | Coqast.Str (loc,a) -> Str (loc,a)
   | Coqast.Path (loc,a) ->
-    let (sl,bn) = repr_path a in
+    let (sl,bn) = Libnames.decode_kn a in
     Path(loc, (List.map string_of_id
                 (List.rev (repr_dirpath sl))) @ [string_of_id bn])
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 9d90782e4d..3be5d8a36a 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -15,6 +15,7 @@ open Ctast;;
 open Termast;;
 open Astterm;;
 open Vernacinterp;;
+open Libnames;;
 open Nametab
 
 open Proof_type;;
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 8c6293ae2c..79375cf2b3 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -8,6 +8,7 @@ open Termast;;
 open Term;;
 open Impargs;;
 open Reduction;;
+open Libnames;;
 open Libobject;;
 open Environ;;
 open Declarations;;
@@ -83,7 +84,7 @@ let implicit_args_to_ast_list sp mipv =
 	| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
 	      
 let convert_qualid qid =
-  let d, id = Nametab.repr_qualid qid in
+  let d, id = Libnames.repr_qualid qid in
     match repr_dirpath d with
 	[] -> nvar id
       | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
@@ -108,7 +109,7 @@ let convert_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
   let envpar = push_rel_context params env in
-  let sp = sp_of_global env (IndRef (sp, tyi)) in
+  let sp = sp_of_global None (IndRef (sp, tyi)) in
   (basename sp,
    convert_env(List.rev params),
    (ast_of_constr true envpar arity),
@@ -167,16 +168,16 @@ let make_definition_ast name c typ implicits =
   ::(implicits_to_ast_list implicits);;
 
 (* This function is inspired by print_constant *)
-let constant_to_ast_list sp =
-  let cb = Global.lookup_constant sp in
+let constant_to_ast_list kn =
+  let cb = Global.lookup_constant kn in
   let c = cb.const_body in
   let typ = cb.const_type in
-  let l = constant_implicits_list sp in
+  let l = constant_implicits_list kn in
   (match c with
       None -> 
-	make_variable_ast (basename sp) typ l
+	make_variable_ast (id_of_label (label kn)) typ l
     | Some c1 ->
-	make_definition_ast (basename sp) c1 typ l)
+	make_definition_ast (id_of_label (label kn)) c1 typ l)
 
 let variable_to_ast_list sp =
   let ((id, c, v), _) = get_variable sp in
@@ -195,13 +196,13 @@ let inductive_to_ast_list sp =
 
 (* this function is inspired by print_leaf_entry from pretty.ml *)
 
-let leaf_entry_to_ast_list (sp,lobj) =
+let leaf_entry_to_ast_list ((sp,kn),lobj) =
   let tag = object_tag lobj in
-  match (sp,tag) with
-  | (_, "VARIABLE") -> variable_to_ast_list (basename sp)
-  | (_, ("CONSTANT"|"PARAMETER")) -> constant_to_ast_list sp
-  | (_, "INDUCTIVE") -> inductive_to_ast_list sp
-  | (_, s) -> 
+  match tag with
+  | "VARIABLE" -> variable_to_ast_list (basename sp)
+  | "CONSTANT"|"PARAMETER" -> constant_to_ast_list kn
+  | "INDUCTIVE" -> inductive_to_ast_list kn
+  | s -> 
       errorlabstrm 
       	"print" (str ("printing of unrecognized object " ^
 		      s ^ " has been required"));;
@@ -210,13 +211,13 @@ let leaf_entry_to_ast_list (sp,lobj) =
 
 
 (* this function is inspired by print_name *)
-let name_to_ast (qid:Nametab.qualid) = 
+let name_to_ast qid = 
   let l = 
     try
       let sp = Nametab.locate_obj qid in
       let (sp,lobj) = 
       	let (sp,entry) =
-          List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
+          List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
       	in
 	  match entry with
             | Lib.Leaf obj -> (sp,obj)
@@ -232,7 +233,7 @@ let name_to_ast (qid:Nametab.qualid) =
 	  | VarRef sp -> variable_to_ast_list sp
   	with Not_found -> 
 	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
-	    let dir,name = Nametab.repr_qualid qid in 
+	    let dir,name = repr_qualid qid in 
 	      if (repr_dirpath dir) <> [] then raise Not_found;
 	      let (_,c,typ) = Global.lookup_named name in 
 		(match c with
@@ -240,12 +241,12 @@ let name_to_ast (qid:Nametab.qualid) =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let sp = Syntax_def.locate_syntactic_definition qid in
+	      let sp = Nametab.locate_syntactic_definition qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
 	      errorlabstrm "print"
-		(Nametab.pr_qualid qid ++
+		(pr_qualid qid ++
 		 spc () ++ str "not a defined object")
   in
   VernacList (List.map (fun x -> (dummy_loc,x)) l)
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 4a68e0134f..600ec5f918 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1,2 @@
-val name_to_ast : Nametab.qualid -> Vernacexpr.vernac_expr;;
-val convert_qualid : Nametab.qualid -> Coqast.t;;
+val name_to_ast : Libnames.qualid -> Vernacexpr.vernac_expr;;
+val convert_qualid : Libnames.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 5bce60f223..61fd060724 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -6,6 +6,8 @@ open Ctast;;
 
 open Pp;;
 
+open Libnames;;
+
 open Library;;
 
 open Ascent;;
@@ -67,7 +69,7 @@ let try_require_module import specif names =
     else Some (specif = "SPECIFICATION"))
    (List.map 
      (fun name ->
-       (dummy_loc,Nametab.make_short_qualid (Names.id_of_string name)))
+       (dummy_loc,Libnames.make_short_qualid (Names.id_of_string name)))
       names)
    (import = "IMPORT")
  with
@@ -110,7 +112,7 @@ let execute_when_necessary v =
       (try 
 	Vernacentries.interp v
        with _ ->
-	 let l=prlist_with_sep spc (fun (_,qid) -> Nametab.pr_qualid qid) l in
+	 let l=prlist_with_sep spc (fun (_,qid) -> pr_qualid qid) l in
 	 msgnl (str "Reinterning of " ++ l ++ str " failed"))
   | VernacRequireFrom (_,_,name,_) ->
       (try 
@@ -427,10 +429,10 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
-      (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
-      read_module (dummy_loc,qid);
+      (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
+      read_library (dummy_loc,qid);
       msg (str "opening... ");
-      import_module false (dummy_loc,qid); 
+      Declaremods.import_module (Nametab.locate_module qid); 
       msgnl (str "done" ++ fnl ());
       ())
  with
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 5dd9d071b5..55aae90be2 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -29,7 +29,7 @@ let get_hyp_by_name g name =
        ("hyp",judgment.uj_type))
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
    Loïc *)
-  with _ -> (let ast = Termast.ast_of_qualid (Nametab.make_short_qualid name)in
+  with _ -> (let ast = Termast.ast_of_qualid (Libnames.make_short_qualid name)in
              let c = Astterm.interp_constr evd env ast in
              ("cste",type_of (Global.env()) Evd.empty c))
 ;;
@@ -252,7 +252,7 @@ let reference dir s =
     Nametab.locate_in_absolute_module dir id
   with Not_found ->
     anomaly ("Coqlib: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 let constant dir s =  Declare.constr_of_reference (reference dir s);;
 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ae876e129f..c7e6be1318 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -6,6 +6,7 @@ open Environ
 open Evd
 open Names
 open Nameops
+open Libnames
 open Term
 open Termops
 open Util
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index d1af58df70..a2620c67f7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -344,9 +344,9 @@ let qualid_to_ct_ID =
     | Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n))
     | _ -> None;;
 
-let tac_qualid_to_ct_ID qid = CT_ident (Nametab.string_of_qualid qid)
+let tac_qualid_to_ct_ID qid = CT_ident (Libnames.string_of_qualid qid)
 
-let loc_qualid_to_ct_ID (_,qid) = CT_ident (Nametab.string_of_qualid qid)
+let loc_qualid_to_ct_ID (_,qid) = CT_ident (Libnames.string_of_qualid qid)
 
 let qualid_or_meta_to_ct_ID = function
   | AN (_,qid) -> tac_qualid_to_ct_ID qid
@@ -360,7 +360,7 @@ let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
 let reference_to_ct_ID = function
   | RIdent (_,id) -> CT_ident (Names.string_of_id id)
-  | RQualid (_,qid) -> CT_ident (Nametab.string_of_qualid qid)
+  | RQualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
 
 let xlate_class = function
   | FunClass -> CT_ident "FUNCLASS"
@@ -437,10 +437,10 @@ let xlate_op the_node opn a b =
   (match a, b with
   | ((Path (_, sl)) :: []), [] ->
     CT_coerce_ID_to_FORMULA(CT_ident
-       (Names.string_of_id (Nameops.basename (section_path sl))))
+       (Names.string_of_label (Names.label (section_path sl))))
   | ((Path (_, sl)) :: []), tl ->
  CT_coerce_ID_to_FORMULA(CT_ident   
-       (Names.string_of_id(Nameops.basename (section_path sl))))
+       (Names.string_of_label(Names.label (section_path sl))))
   | _, _ -> xlate_error "xlate_op : CONST")
  | (** string_of_path needs to be investigated.
     *)
@@ -454,8 +454,8 @@ let xlate_op the_node opn a b =
 		  | _ -> assert false
 	    else
 	    CT_coerce_ID_to_FORMULA(
-	      CT_ident(Names.string_of_id
-			 (Nameops.basename (section_path sl))))
+	      CT_ident(Names.string_of_label
+			 (Names.label (section_path sl))))
   	| _, _ -> xlate_error "xlate_op : MUTIND")
  | "CASE"
  | "MATCH" ->
@@ -478,7 +478,10 @@ let xlate_op the_node opn a b =
 	 | Some(Rform x) -> x
 	 | _ -> assert false
    else
-   let name = Names.string_of_path (section_path sl) in
+   let name = 
+     let dir,id = Libnames.decode_kn (section_path sl) in
+       Names.string_of_dirpath (Libnames.extend_dirpath dir id) 
+   in
      (* This is rather a patch to cope with the fact that identifier
         names have disappeared from the vo files for grammar rules *)
        let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -2864,7 +2867,7 @@ let xlate_vernac =
 (*
      | "EndSection", ((Varg_ident id) :: []) ->
 *)
-  | VernacEndSection id -> CT_section_end (xlate_ident id)
+  | VernacEndSegment id -> CT_section_end (xlate_ident id)
 (*
      | "StartProof",
          ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) ->
@@ -3249,9 +3252,9 @@ let xlate_vernac =
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Nametab.DischargeAt _ -> CT_local
-       | Nametab.NotDeclare -> assert false in
+       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Libnames.DischargeAt _ -> CT_local
+       | Libnames.NotDeclare -> assert false in
       CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
         xlate_class id2, xlate_class id3)
 
@@ -3260,9 +3263,9 @@ let xlate_vernac =
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Nametab.DischargeAt _ -> CT_local 
-       | Nametab.NotDeclare -> assert false in
+       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Libnames.DischargeAt _ -> CT_local 
+       | Libnames.NotDeclare -> assert false in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
 (* Not supported