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

8 files changed, 34 insertions, 21 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index a915148a31..5024d515d7 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -18,7 +18,11 @@ open Pretyping
 open Evarutil
 open Ast
 open Coqast
-open Pretype_errors
+open Nametab
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SyntacticDef of section_path
 
 (*Takes a list of variables which must not be globalized*)
 let from_list l = List.fold_right Idset.add l Idset.empty
@@ -243,9 +247,8 @@ let ast_to_var (env,impls) (vars1,vars2) loc s =
 (* This is generic code to deal with globalization                  *)
 
 type 'a globalization_action = {
-  parse_var : string -> 'a;
-  parse_ref : global_reference -> 'a;
-  parse_syn : section_path -> 'a;
+  parse_var : identifier -> 'a;
+  parse_ref : extended_global_reference -> 'a;
   fail : qualid -> 'a * int list;
 }
 
@@ -253,18 +256,18 @@ let translate_qualid act qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],s -> act.parse_var (string_of_id s), []
+      | [],id -> act.parse_var id, []
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference? *)
   try
     let ref = Nametab.locate qid in
-    act.parse_ref ref, implicits_of_global ref
+    act.parse_ref (TrueGlobal ref), implicits_of_global ref
   with Not_found ->
   (* Is it a reference to a syntactic definition? *)
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
-    act.parse_syn sp, []
+    act.parse_ref (SyntacticDef sp), []
   with Not_found ->
     act.fail qid
 
@@ -274,7 +277,7 @@ let rawconstr_of_var env vars loc s =
   try
     ast_to_var env vars loc s
   with Not_found ->
-    error_var_not_found_loc loc CCI (id_of_string s)
+    Pretype_errors.error_var_not_found_loc loc CCI (id_of_string s)
 
 let rawconstr_of_qualid env vars loc qid =
   (* Is it a bound variable? *)
@@ -564,7 +567,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 (* Globalization of AST quotations (mainly used to get statically         *)
 (* bound idents in grammar or pretty-printing rules)                      *)
 (**************************************************************************)
-
+(*
 (* A brancher ultérieurement sur Termast.ast_of_ref *)
 let ast_of_ref loc = function
   | ConstRef sp -> Node (loc, "CONST", [path_section loc sp])
@@ -572,11 +575,19 @@ let ast_of_ref loc = function
         Node (loc, "MUTCONSTRUCT", [path_section loc sp; num i; num j])
   | IndRef (sp, i) -> Node (loc, "MUTIND", [path_section loc sp; num i])
   | VarRef sp -> failwith "ast_of_ref: TODO"
+*)
+let ast_of_ref_loc loc ref = set_loc loc (Termast.ast_of_ref ref)
 
 let ast_of_syndef loc sp = Node (loc, "SYNCONST", [path_section loc sp])
 
-let ast_of_var env ast s =
-  if isMeta s or Idset.mem (id_of_string s) env then ast
+let ast_of_extended_ref_loc loc = function
+  | TrueGlobal ref -> ast_of_ref_loc loc ref
+  | SyntacticDef sp -> ast_of_syndef loc sp
+
+let ast_of_extended_ref = ast_of_extended_ref_loc dummy_loc
+
+let ast_of_var env ast id =
+  if isMeta (string_of_id id) or Idset.mem id env then ast
   else raise Not_found
 
 let ast_hole = Node (dummy_loc, "ISEVAR", [])
@@ -606,8 +617,7 @@ let ast_adjust_consts sigma =
   and adjust_qualid env loc ast sp =
     let act = {
       parse_var = ast_of_var env ast;
-      parse_ref = ast_of_ref loc;
-      parse_syn = ast_of_syndef loc;
+      parse_ref = ast_of_extended_ref_loc loc;
       fail = warning_globalize ast } in
     fst (translate_qualid act sp)
 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 613b3c1240..cf2cbfd510 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -65,7 +65,7 @@ val globalize_ast    : Coqast.t -> Coqast.t
 
 (* This transforms args of a qualid keyword into a qualified ident *)
 (* it does no relocation *)
-val interp_qualid : Coqast.t list -> qualid
+val interp_qualid : Coqast.t list -> Nametab.qualid
 
 (* Translation rules from V6 to V7:
 
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index b0a7f3a8a2..d7e8efa20f 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -6,6 +6,7 @@ open Names
 open Term
 open Declare
 open Pattern
+open Nametab
 
 let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
 let myvar_path =
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 34d3d29803..1e45d0ea25 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -15,6 +15,7 @@ open Declare
 open Impargs
 open Libobject
 open Printer
+open Nametab
 
 let print_basename sp = pr_global (ConstRef sp)
 
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index c224bc20db..7b4ea47e83 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -21,15 +21,15 @@ val print_context : bool -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds
 val print_full_context : unit -> std_ppcmds
 val print_full_context_typ : unit -> std_ppcmds
-val print_sec_context : qualid -> std_ppcmds
-val print_sec_context_typ : qualid -> std_ppcmds
+val print_sec_context : Nametab.qualid -> std_ppcmds
+val print_sec_context_typ : Nametab.qualid -> std_ppcmds
 val print_val : env -> unsafe_judgment -> std_ppcmds
 val print_type : env -> unsafe_judgment -> std_ppcmds
 val print_eval :
   'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
 val print_mutual : section_path -> std_ppcmds
-val print_name : qualid -> std_ppcmds
-val print_opaque_name : qualid -> std_ppcmds
+val print_name : Nametab.qualid -> std_ppcmds
+val print_opaque_name : Nametab.qualid -> std_ppcmds
 val print_local_context : unit -> std_ppcmds
 
 (*i
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d0535fbac5..a325f1a8b1 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -21,8 +21,8 @@ let pr_global ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
   paresseusement : il faut forcer l'évaluation pour capturer
   l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
-  let qid = Global.qualid_of_global ref in
-  [< 'sTR (string_of_qualid qid) >]
+  let s = Global.string_of_global ref in
+  [< 'sTR s >]
 
 let global_const_name sp =
   try pr_global (ConstRef sp)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 5b0675d979..56f330b749 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -15,6 +15,7 @@ open Coqast
 open Ast
 open Rawterm
 open Pattern
+open Nametab
 
 (* In this file, we translate rawconstr to ast, in order to print constr *)
 
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 1d6ee2208a..35a7349d8f 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -27,7 +27,7 @@ val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t
 val ast_of_inductive    : env -> inductive -> Coqast.t
 val ast_of_ref          : global_reference -> Coqast.t
-val ast_of_qualid       : qualid -> Coqast.t
+val ast_of_qualid       : Nametab.qualid -> Coqast.t
 
 (* For debugging *)
 val print_implicits : bool ref