Déplacement de qualid dans Nametab, hors du noyau

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

9 files changed, 37 insertions, 26 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5fce67d51..4d1a2e2ad 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -300,13 +300,13 @@ let push_inductive_names ccitab sp mie =
 
 let cache_end_section (_,(sp,mc)) =
   Nametab.push_section sp mc;
-  Nametab.open_section_contents (qualid_of_sp sp)
+  Nametab.open_section_contents (Nametab.qualid_of_sp sp)
 
 let load_end_section (_,(sp,mc)) =
   Nametab.push_module sp mc
 
 let open_end_section (_,(sp,_)) =
-  Nametab.rec_open_module_contents (qualid_of_sp sp)
+  Nametab.rec_open_module_contents (Nametab.qualid_of_sp sp)
 
 let (in_end_section, out_end_section) =
   declare_object
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index cde9421d0..f04e99e79 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -63,6 +63,11 @@ let rec explain_exn_default = function
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
   | Logic.RefinerError e -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >]
+  | Nametab.GlobalizationError q ->
+      hOV 0 [< 'sTR "Error:"; 'sPC;
+	       'sTR "The reference"; 'sPC; Nametab.pr_qualid q;
+	       'sPC ; 'sTR "was not found"; 
+	       'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
   | Tacmach.FailError i ->
       hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; 
 	       'iNT i; 'sTR")." >]
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f87a5b213..4a9c134f9 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -279,11 +279,6 @@ let explain_var_not_found k ctx id =
      'sPC ; 'sTR "was not found"; 
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
-let explain_global_not_found k ctx q = 
-  [< 'sTR "The reference"; 'sPC; pr_qualid q;
-     'sPC ; 'sTR "was not found"; 
-     'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
-
 (* Pattern-matching errors *)
 let explain_bad_pattern k ctx cstr ty = 
   let pt = prterm_env ctx ty in
@@ -360,8 +355,6 @@ let explain_type_error k ctx = function
       explain_not_clean k ctx n c
   | VarNotFound id ->
       explain_var_not_found k ctx id
-  | QualidNotFound sp ->
-      explain_global_not_found k ctx sp
   | UnexpectedType (actual,expected) ->
       explain_unexpected_type k ctx actual expected
   | NotProduct c ->
@@ -506,3 +499,4 @@ let explain_inductive_error = function
   | NotAllowedCaseAnalysis (dep,k,i) -> error_not_allowed_case_analysis dep k i
   | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
   | NotMutualInScheme -> error_not_mutual_in_scheme ()
+
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d0eb926a4..d95e254c8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -224,8 +224,8 @@ let add_infix assoc n inf pr =
     errorlabstrm "Vernacentries.infix_grammar_entry"
       [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >];
   (* check the grammar entry *)
-  let prefast = Astterm.globalize_constr (Termast.ast_of_qualid pr) in
-  let prefname = (Names.string_of_qualid pr)^"_infix" in
+  let prefast = Termast.ast_of_ref pr in
+  let prefname = (Names.string_of_path (Global.sp_of_global pr))^"_infix" in
   let gram_rule = gram_infix assoc n (split inf) prefname prefast in
   (* check the syntax entry *)
   let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in
@@ -273,7 +273,7 @@ let distfix assoc n sl fname astf  =
   }
 
 let add_distfix a n df f =
-  let fname = (Names.string_of_qualid f)^"_distfix" in
-  let astf = Astterm.globalize_constr (Termast.ast_of_qualid f) in
+  let fname = (Names.string_of_path (Global.sp_of_global f))^"_distfix" in
+  let astf = Termast.ast_of_ref f in
   Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, []))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index fc4ef2968..08fb2800d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Extend
 open Names
+open Term
 (*i*)
 
 (* Adding grammar and pretty-printing objects in the environment *)
@@ -13,7 +14,9 @@ val add_syntax_obj : string -> Coqast.t list -> unit
 val add_grammar_obj : string -> Coqast.t list -> unit
 val add_token_obj : string -> unit
 
-val add_infix : Gramext.g_assoc option -> int -> string -> qualid -> unit
-val add_distfix : Gramext.g_assoc option -> int -> string -> qualid -> unit
+val add_infix :
+  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+val add_distfix :
+  Gramext.g_assoc option -> int -> string -> global_reference -> unit
 
 val print_grammar : string -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 49042811a..11e65b934 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -33,6 +33,7 @@ open Tactic_debug
 open Command
 open Goptions
 open Mltop
+open Nametab
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
 let join_binders binders = 
@@ -108,7 +109,14 @@ let show_top_evars () =
 (* Locate commands *)
 let locate_qualid loc qid =
   try Nametab.locate qid
-  with Not_found -> Pretype_errors.error_global_not_found_loc loc qid
+  with Not_found -> 
+  try
+    let _ = Syntax_def.locate_syntactic_definition qid in
+    error
+      ("Unexpected reference to a syntactic definition: "
+       ^(string_of_qualid qid))
+  with Not_found ->
+    Nametab.error_global_not_found_loc loc qid
 
  (* Pour pcoq *)
 let global = locate_qualid
@@ -180,7 +188,7 @@ let _ =
        | [VARG_STRING dir] ->
 	   (fun () -> add_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
-           let aliasdir,aliasname = repr_qualid alias in
+           let aliasdir,aliasname = Nametab.repr_qualid alias in
 	    (fun () -> add_path dir (aliasdir@[string_of_id aliasname]))
        | _ -> bad_vernac_args "ADDPATH")
 
@@ -197,7 +205,7 @@ let _ =
        | [VARG_STRING dir] ->
 	   (fun () -> add_rec_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
-           let aliasdir,aliasname = repr_qualid alias in
+           let aliasdir,aliasname = Nametab.repr_qualid alias in
 	    (fun () ->
 	       let alias = aliasdir@[string_of_id aliasname] in
 	       add_rec_path dir alias;
@@ -631,8 +639,7 @@ let _ =
        List.iter
 	 (function 
 	    | VARG_CONSTANT sp ->
-		warning_opaque
-		  (string_of_qualid (Global.qualid_of_global (ConstRef sp)));
+		warning_opaque (Global.string_of_global (ConstRef sp));
 		Global.set_opaque sp
 	    |   _  -> bad_vernac_args "OPAQUE")
 	 id_list)
@@ -1463,7 +1470,8 @@ let _ =
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] ->
            (fun () ->
-	      Metasyntax.add_infix (Extend.gram_assoc assoc) n inf pref)
+	      let ref = global dummy_loc pref in
+	      Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref)
        | _ -> bad_vernac_args "INFIX")
 
 let _ =
@@ -1471,7 +1479,8 @@ let _ =
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] ->
            (fun () ->
-              Metasyntax.add_distfix (Extend.gram_assoc assoc) n s pref)
+	      let ref = global dummy_loc pref in
+              Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref)
        | _ -> bad_vernac_args "DISTFIX")
 
 let _ =
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 5efd2bd40..f1a93824c 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -26,7 +26,7 @@ val get_current_context_of_args : vernac_arg list -> Proof_type.enamed_declarati
 (* This function is used to transform a qualified identifier into a
    global reference, with a nice error message in case of failure.
    It is used in pcoq. *)
-val global : Coqast.loc -> qualid -> global_reference;;
+val global : Coqast.loc -> Nametab.qualid -> global_reference;;
 
 (* this function is used to analyse the extra arguments in search commands.
    It is used in pcoq. *)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index a6538bc1b..e4595244a 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -24,7 +24,7 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
-  | VARG_QUALID of qualid
+  | VARG_QUALID of Nametab.qualid
   | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
@@ -84,7 +84,7 @@ let rec cvt_varg ast =
 	let q = Astterm.interp_qualid p in
 	let sp =
 	  try Nametab.locate_constant q
-	  with Not_found -> Pretype_errors.error_global_not_found_loc loc q
+	  with Not_found -> Nametab.error_global_not_found_loc loc q
 	in VARG_CONSTANT sp
     | Str(_,s) -> VARG_STRING s
     | Num(_,n) -> VARG_NUMBER n
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 0c136820a..5863ffb7b 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -20,7 +20,7 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
-  | VARG_QUALID of qualid
+  | VARG_QUALID of Nametab.qualid
   | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t