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

45 files changed, 257 insertions, 213 deletions

diff --git a/.depend b/.depend
index 4ff2a8547d..f2312836bf 100644
--- a/.depend
+++ b/.depend
@@ -29,14 +29,14 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
-    library/libobject.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
+    library/libobject.cmi kernel/names.cmi library/nametab.cmi \
+    kernel/sign.cmi kernel/term.cmi 
 library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+    library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi 
 library/goptions.cmi: kernel/names.cmi lib/pp.cmi 
 library/impargs.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/term.cmi 
@@ -46,14 +46,17 @@ library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi
 library/libobject.cmi: kernel/names.cmi 
 library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi lib/system.cmi 
-library/nametab.cmi: library/libobject.cmi kernel/names.cmi kernel/term.cmi \
-    lib/util.cmi 
+library/nametab.cmi: library/libobject.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi lib/util.cmi 
 library/summary.cmi: kernel/names.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
-    library/impargs.cmi kernel/names.cmi pretyping/pattern.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
+    library/impargs.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
 parsing/coqlib.cmi: pretyping/pattern.cmi kernel/term.cmi 
 parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -66,16 +69,16 @@ parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
 parsing/pretty.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi 
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/sign.cmi kernel/term.cmi 
 parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
     pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     kernel/term.cmi 
 parsing/search.cmi: kernel/environ.cmi kernel/names.cmi pretyping/pattern.cmi \
     lib/pp.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
-    pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi 
+    library/nametab.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \
+    kernel/sign.cmi kernel/term.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/inductive.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/term.cmi 
@@ -107,7 +110,8 @@ pretyping/recordops.cmi: pretyping/classops.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi kernel/term.cmi 
 pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
     kernel/term.cmi 
-pretyping/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi 
+pretyping/syntax_def.cmi: kernel/names.cmi library/nametab.cmi \
+    pretyping/rawterm.cmi 
 pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/term.cmi 
 pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
@@ -126,8 +130,8 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \
     lib/stamps.cmi kernel/term.cmi lib/util.cmi 
 proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
-    lib/util.cmi 
+    kernel/names.cmi library/nametab.cmi lib/stamps.cmi pretyping/tacred.cmi \
+    kernel/term.cmi lib/util.cmi 
 proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
@@ -141,7 +145,7 @@ proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \
     proofs/proof_type.cmi kernel/term.cmi 
 tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/names.cmi pretyping/pattern.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    lib/pp.cmi proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
 tactics/autorewrite.cmi: parsing/coqast.cmi proofs/tacmach.cmi \
     kernel/term.cmi 
@@ -195,12 +199,12 @@ toplevel/recordobj.cmi: kernel/term.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
     kernel/names.cmi proofs/proof_type.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 contrib/extraction/close_env.cmi: kernel/names.cmi kernel/term.cmi 
 contrib/extraction/extraction.cmi: contrib/extraction/miniml.cmi \
     kernel/names.cmi kernel/term.cmi 
@@ -215,18 +219,16 @@ config/coq_config.cmo: config/coq_config.cmi
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
 dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx 
-dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
-    toplevel/command.cmi kernel/environ.cmi toplevel/errors.cmi \
-    kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \
-    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi kernel/univ.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacinterp.cmi 
-dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
-    toplevel/command.cmx kernel/environ.cmx toplevel/errors.cmx \
-    kernel/evd.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \
-    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx kernel/univ.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacinterp.cmx 
+dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \
+    toplevel/errors.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/refiner.cmi \
+    kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \
+    parsing/termast.cmi kernel/univ.cmi toplevel/vernacinterp.cmi 
+dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \
+    toplevel/errors.cmx kernel/evd.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/refiner.cmx \
+    kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \
+    parsing/termast.cmx kernel/univ.cmx toplevel/vernacinterp.cmx 
 kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
     kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi kernel/closure.cmi 
@@ -331,30 +333,22 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
 lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi 
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -429,6 +423,14 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -761,54 +763,52 @@ proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \
     pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi 
 proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \
     pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi library/global.cmi kernel/names.cmi lib/pp.cmi \
-    parsing/pretty.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    kernel/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \
+    lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi proofs/proof_type.cmi \
     kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
     parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/proof_trees.cmi 
 proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \
     pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    kernel/evd.cmx library/global.cmx kernel/names.cmx lib/pp.cmx \
-    parsing/pretty.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    kernel/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \
+    lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx proofs/proof_type.cmx \
     kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \
     parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/proof_trees.cmi 
 proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
-    lib/util.cmi proofs/proof_type.cmi 
+    kernel/names.cmi library/nametab.cmi lib/stamps.cmi pretyping/tacred.cmi \
+    kernel/term.cmi lib/util.cmi proofs/proof_type.cmi 
 proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/names.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \
-    lib/util.cmx proofs/proof_type.cmi 
+    kernel/names.cmx library/nametab.cmx lib/stamps.cmx pretyping/tacred.cmx \
+    kernel/term.cmx lib/util.cmx proofs/proof_type.cmi 
 proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi kernel/type_errors.cmi \
-    lib/util.cmi proofs/refiner.cmi 
+    library/global.cmi kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
+    kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi 
 proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    kernel/sign.cmx lib/stamps.cmx kernel/term.cmx kernel/type_errors.cmx \
-    lib/util.cmx proofs/refiner.cmi 
+    library/global.cmx kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
+    kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi 
 proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
     parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
     lib/dyn.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     lib/gmap.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \
-    proofs/pfedit.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    proofs/tactic_debug.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    proofs/tacinterp.cmi 
+    proofs/pfedit.cmi lib/pp.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi 
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
     lib/dyn.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
     lib/gmap.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \
-    proofs/pfedit.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
-    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/sign.cmx \
-    library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    proofs/tactic_debug.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    proofs/tacinterp.cmi 
+    proofs/pfedit.cmx lib/pp.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx proofs/tactic_debug.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi 
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
     kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi library/global.cmi kernel/instantiate.cmi proofs/logic.cmi \
@@ -892,15 +892,17 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
 tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi kernel/evd.cmi \
-    kernel/instantiate.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+    kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
 tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx kernel/evd.cmx \
-    kernel/instantiate.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+    kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
+    pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx 
 tactics/elim.cmo: proofs/clenv.cmi tactics/hiddentac.cmi \
     tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
@@ -1059,10 +1061,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
@@ -1132,13 +1134,13 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
     library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/discharge.cmi 
 toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/indtypes.cmi \
-    parsing/lexer.cmi proofs/logic.cmi lib/options.cmi lib/pp.cmi \
-    proofs/tacmach.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
-    toplevel/errors.cmi 
+    parsing/lexer.cmi proofs/logic.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi proofs/tacmach.cmi kernel/type_errors.cmi kernel/univ.cmi \
+    lib/util.cmi toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/indtypes.cmx \
-    parsing/lexer.cmx proofs/logic.cmx lib/options.cmx lib/pp.cmx \
-    proofs/tacmach.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
-    toplevel/errors.cmi 
+    parsing/lexer.cmx proofs/logic.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx proofs/tacmach.cmx kernel/type_errors.cmx kernel/univ.cmx \
+    lib/util.cmx toplevel/errors.cmi 
 toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi 
@@ -1223,14 +1225,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    toplevel/discharge.cmi library/library.cmi lib/options.cmi \
-    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \
-    lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    toplevel/discharge.cmx library/library.cmx lib/options.cmx \
-    parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx library/states.cmx \
-    lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
     parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
@@ -1275,6 +1269,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    toplevel/discharge.cmi library/library.cmi lib/options.cmi \
+    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \
+    lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    toplevel/discharge.cmx library/library.cmx lib/options.cmx \
+    parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx library/states.cmx \
+    lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/extraction/close_env.cmo: kernel/names.cmi kernel/term.cmi \
     contrib/extraction/close_env.cmi 
 contrib/extraction/close_env.cmx: kernel/names.cmx kernel/term.cmx \
@@ -1365,8 +1367,6 @@ contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     kernel/reduction.cmx library/summary.cmx proofs/tacmach.cmx \
     pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
     kernel/environ.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
@@ -1385,6 +1385,8 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/xml/xmlcommand.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
 parsing/lexer.cmo: 
 parsing/q_coqast.cmo: 
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 00ce6d2078..821c4b2021 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -217,7 +217,8 @@ let constant dir s =
   try 
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir id)))
+    anomaly ("Coq_omega: cannot find "^
+	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let zarith_constant dir = constant ("Zarith"::dir)
 
@@ -373,12 +374,13 @@ let make_coq_path dir s =
   let ref = 
     try Nametab.locate_in_absolute_module dir id 
     with Not_found ->
-      anomaly("Coq_omega: cannot find "^(string_of_qualid(make_qualid dir id)))
+      anomaly("Coq_omega: cannot find "^
+	      (Nametab.string_of_qualid(Nametab.make_qualid dir id)))
   in
   match ref with
     | ConstRef sp -> EvalConstRef sp
     | _ -> anomaly ("Coq_omega: "^
-		    (string_of_qualid (make_qualid dir id))^
+		    (Nametab.string_of_qualid (Nametab.make_qualid dir id))^
 		    " is not a constant")
 
 let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs")
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index efc8d78d85..ac3af30b8d 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -118,7 +118,8 @@ let constant dir s =
   try 
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Quote: cannot find "^(string_of_qualid (make_qualid dir id)))
+    anomaly ("Quote: cannot find "^
+	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 1cfbf965cc..0e200313c7 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -31,7 +31,8 @@ let constant dir s =
   try 
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir id)))
+    anomaly ("Ring: cannot find "^
+	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 (* Ring_theory *)
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 0f55481c32..906cf8b078 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -694,7 +694,7 @@ let pp_cmds_of_inner_types inner_types target_uri =
 let print sp fn =
  let module D = Declarations in
  let module G = Global in
- let module N = Names in
+ let module N = Nametab in
  let module T = Term in
  let module X = Xml in
   let (_,id) = N.repr_qualid sp in
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 827cb34f64..1c9b22070a 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -21,7 +21,7 @@
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-val print : Names.qualid -> string option -> unit
+val print : Nametab.qualid -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7cb08e06b4..998ad3054e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -252,7 +252,7 @@ let print_pure_constr csr =
 
   in
      box_display csr; print_newline()
-
+(*
 let _ =
   Vernacentries.add "PrintConstr"
     (function
@@ -270,3 +270,4 @@ let _ =
               let (evmap,sign) = Command.get_current_context () in
   	      print_pure_constr (Astterm.interp_constr evmap sign c))
        | _ -> bad_vernac_args "PrintPureConstr")
+*)
diff --git a/kernel/names.ml b/kernel/names.ml
index 83cea889a4..035a5d5059 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -254,16 +254,6 @@ let kind_of_string = function
   | "obj" -> OBJ
   | _ -> invalid_arg "kind_of_string"
 
-(*s Section paths *)
-
-type qualid = string list * identifier
-
-let make_qualid p s = (p,s)
-let repr_qualid q = q
-
-let string_of_qualid (l,s) = String.concat "." (l@[s])
-let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
-
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
@@ -281,9 +271,6 @@ let kind_of_path sp = sp.kind
 let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
-let qualid_of_sp sp =
-  make_qualid (dirpath sp) (string_of_id (basename sp))
-
 (* parsing and printing of section paths *)
 let string_of_dirpath sl = String.concat "." sl
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 6912d66654..98e39fae93 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -57,15 +57,6 @@ type dir_path = string list
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
-(*s Qualified idents are names relative to the current visilibity of names *)
-type qualid
-
-val make_qualid : dir_path -> identifier -> qualid
-val repr_qualid : qualid -> dir_path * identifier
-
-val string_of_qualid : qualid -> string
-val pr_qualid : qualid -> std_ppcmds
-
 (*s Section paths are {\em absolute} names *)
 type section_path
 
@@ -81,9 +72,6 @@ val kind_of_path : section_path -> path_kind
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
-(* Turns an absolute name into a qualified name denoting the same name *)
-val qualid_of_sp : section_path -> qualid
-
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 269e30fca7..225756a999 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -59,8 +59,6 @@ type type_error =
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
-  (* Relocation error *)
-  | QualidNotFound of qualid
 
 exception TypeError of path_kind * env * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 22c6bff998..e7e850c714 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -63,8 +63,6 @@ type type_error =
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
-  (* Relocation error *)
-  | QualidNotFound of qualid
 
 exception TypeError of path_kind * env * type_error
 
diff --git a/library/declare.ml b/library/declare.ml
index 853a22d121..f0f2790a57 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -15,6 +15,7 @@ open Libobject
 open Lib
 open Impargs
 open Indrec
+open Nametab
 
 type strength = 
   | NotDeclare
diff --git a/library/declare.mli b/library/declare.mli
index 07dc969142..6c47e3a52a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -90,11 +90,11 @@ val extract_instance : global_reference -> constr array -> constr array
 val constr_of_reference :
   'a Evd.evar_map -> Environ.env -> global_reference -> constr
 
-val global_qualified_reference : qualid -> constr
+val global_qualified_reference : Nametab.qualid -> constr
 val global_absolute_reference : section_path -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
-val construct_qualified_reference : Environ.env -> qualid -> constr
+val construct_qualified_reference : Environ.env -> Nametab.qualid -> constr
 val construct_absolute_reference : Environ.env -> section_path -> constr
 
 (* This should eventually disappear *)
diff --git a/library/global.ml b/library/global.ml
index cdc7fdb18d..faca388aa1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -57,7 +57,7 @@ let import cenv = global_env := import cenv !global_env
 
 (* Some instanciations of functions from [Environ]. *)
 
-let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id
+let sp_of_global ref = Environ.sp_of_global (env_of_safe_env !global_env) ref
 
 (* To know how qualified a name should be to be understood in the current env*)
 
@@ -65,14 +65,16 @@ let qualid_of_global ref =
   let sp = sp_of_global ref in
   let id = basename sp in
   let rec find_visible dir qdir =
-    let qid = make_qualid qdir id in
+    let qid = Nametab.make_qualid qdir id in
     if (try Nametab.locate qid = ref with Not_found -> false) then qid
     else match dir with
-      | [] -> qualid_of_sp sp
+      | [] -> Nametab.qualid_of_sp sp
       | a::l -> find_visible l (a::qdir)
   in
   find_visible (List.rev (dirpath sp)) []
 
+let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
+
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
diff --git a/library/global.mli b/library/global.mli
index 74a7197d4b..da0386be1d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -49,7 +49,10 @@ val import : compiled_env -> unit
 (*s Some functions of [Environ] instanciated on the global environment. *)
 
 val sp_of_global : global_reference -> section_path
-val qualid_of_global : global_reference -> qualid
+
+(*s This is for printing purpose *)
+val qualid_of_global : global_reference -> Nametab.qualid
+val string_of_global : global_reference -> string
 
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
diff --git a/library/library.ml b/library/library.ml
index 0ec028963f..d1e162affc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -8,6 +8,7 @@ open Names
 open Environ
 open Libobject
 open Lib
+open Nametab
 
 (*s Load path. *)
 
@@ -27,7 +28,7 @@ type module_disk = {
   md_name : string;
   md_compiled_env : compiled_env;
   md_declarations : library_segment;
-  md_nametab : Nametab.module_contents;
+  md_nametab : module_contents;
   md_deps : (string * Digest.t * bool) list }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -38,7 +39,7 @@ type module_t = {
   module_filename : load_path_entry * string;
   module_compiled_env : compiled_env;
   module_declarations : library_segment;
-  module_nametab : Nametab.module_contents;
+  module_nametab : module_contents;
   mutable module_opened : bool;
   mutable module_exported : bool;
   module_deps : (string * Digest.t * bool) list;
@@ -117,7 +118,7 @@ let rec open_module force s =
   if force or not m.module_opened then begin
     List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps;
     open_objects m.module_declarations;
-    Nametab.open_module_contents (make_qualid [] (id_of_string s)); 
+    open_module_contents (make_qualid [] (id_of_string s)); 
     m.module_opened <- true
   end
 
@@ -155,7 +156,7 @@ let rec load_module_from s f =
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
     let sp = Names.make_path lpe.coq_dirpath (id_of_string s) CCI in
-    Nametab.push_module sp m.module_nametab;
+    push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table;
     m
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 046a9518ce..2534837916 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -8,6 +8,23 @@ open Libobject
 open Declarations
 open Term
 
+(*s qualified names *)
+type qualid = string list * identifier
+
+let make_qualid p id = (p,id)
+let repr_qualid q = q
+
+let string_of_qualid (l,id) = String.concat "." (l@[string_of_id id])
+let pr_qualid (l,id) =
+  prlist_with_sep (fun () -> pr_str ".") pr_str (l@[string_of_id id])
+
+let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
+
+exception GlobalizationError of qualid
+
+let error_global_not_found_loc loc q =
+  Stdpp.raise_with_loc loc (GlobalizationError q)
+
 (*s Roots of the space of absolute names *)
 
 let roots = ref []
diff --git a/library/nametab.mli b/library/nametab.mli
index a9a466bb3e..a62385bb66 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -3,18 +3,40 @@
 
 (*i*)
 open Util
+open Pp
 open Names
 open Term
 (*i*)
 
-(* This module contains the table for globalization, which associates global
-   names (section paths) to identifiers. *)
+(*s This module contains the table for globalization, which associates global
+   names (section paths) to qualified names. *)
 
+(*s A [qualid] is a partially qualified ident; it includes fully
+    qualified names (= absolute names) and all intermediate partial
+    qualifications of absolute names, including single identifiers *)
+type qualid
+
+val make_qualid : dir_path -> identifier -> qualid
+val repr_qualid : qualid -> dir_path * identifier
+
+val string_of_qualid : qualid -> string
+val pr_qualid : qualid -> std_ppcmds
+
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+exception GlobalizationError of qualid
+
+(* Raises a globalization error *)
+val error_global_not_found_loc : loc -> qualid -> 'a
+
+(*s Names tables *)
 type cci_table = global_reference Idmap.t
 type obj_table = (section_path * Libobject.obj) Idmap.t
 type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
+(*s Registers absolute paths *)
 val push : section_path -> global_reference -> unit
 val push_object : section_path -> Libobject.obj -> unit
 val push_module : section_path -> module_contents -> unit
@@ -25,6 +47,8 @@ val push_local_object : section_path -> Libobject.obj -> unit
 (* This should eventually disappear *)
 val sp_of_id : path_kind -> identifier -> global_reference
 
+(*s The following functions perform globalization of qualified names *)
+
 (* This returns the section path of a constant or fails with [Not_found] *)
 val constant_sp_of_id : identifier -> section_path
 
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
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ca85535252..630a8bb310 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -232,9 +232,9 @@ let strength_of_cl = function
 let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
-  | CL_CONST sp -> string_of_qualid (Global.qualid_of_global (ConstRef sp))
-  | CL_IND sp -> string_of_qualid (Global.qualid_of_global (IndRef sp))
-  | CL_SECVAR sp -> string_of_qualid (Global.qualid_of_global (VarRef sp))
+  | CL_CONST sp -> Global.string_of_global (ConstRef sp)
+  | CL_IND sp -> Global.string_of_global (IndRef sp)
+  | CL_SECVAR sp -> Global.string_of_global (VarRef sp)
 
 (* coercion_value : int -> unsafe_judgment * bool *)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index dbc717fc0d..ff57b0012c 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -13,9 +13,6 @@ let raise_pretype_error (loc,k,ctx,te) =
 let error_var_not_found_loc loc k s =
   raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s)
 
-let error_global_not_found_loc loc q =
-  raise_pretype_error (loc,CCI, Global.env() (*bidon*), QualidNotFound q)
-
 let error_cant_find_case_type_loc loc env expr =
   raise_pretype_error (loc, CCI, env, CantFindCaseType expr)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 88f5889eba..a48329bd18 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -16,9 +16,6 @@ open Rawterm
 val error_var_not_found_loc :
   loc -> path_kind -> identifier -> 'a
 
-val error_global_not_found_loc :
-  loc -> qualid -> 'a
-
 val error_cant_find_case_type_loc : 
   loc -> env -> constr -> 'a
 
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index 84ef5e1d9e..cbe1ba7e5c 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -12,6 +12,6 @@ val declare_syntactic_definition : identifier -> rawconstr -> unit
 
 val search_syntactic_definition : section_path -> rawconstr
 
-val locate_syntactic_definition : qualid -> section_path
+val locate_syntactic_definition : Nametab.qualid -> section_path
 
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1b4b89f8bf..d942a66114 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -593,7 +593,7 @@ let unfold env sigma name =
 
 let string_of_evaluable_ref = function
   | EvalVarRef id -> string_of_id id
-  | EvalConstRef sp -> string_of_qualid (qualid_of_sp sp)
+  | EvalConstRef sp -> string_of_path sp
 
 (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8a655b3da2..4a8f8dfc6c 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -389,7 +389,7 @@ let ast_of_cvt_redexp = function
 (* Gives the ast corresponding to a tactic argument *)
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar (string_of_id id) 
-  | Qualid qid      -> nvar (string_of_qualid qid) 
+  | Qualid qid      -> nvar (Nametab.string_of_qualid qid) 
   | Quoted_string s -> str s
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 319b7ff4f9..3f5dbaeea7 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -88,7 +88,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
-  | Qualid         of qualid
+  | Qualid         of Nametab.qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index e49faeb58e..3a9f32b639 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -120,7 +120,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
-  | Qualid         of qualid
+  | Qualid         of Nametab.qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 9f68b896fe..cd7252c442 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -185,7 +185,7 @@ let look_for_interp = Hashtbl.find interp_tab
 let glob_const_nvar loc env qid =
   try
     (* We first look for a variable of the current proof *)
-    match repr_qualid qid with
+    match Nametab.repr_qualid qid with
       | [],id ->
 	  (* lookup_value may raise Not_found *)
 	  (match Environ.lookup_named_value id env with
@@ -201,10 +201,10 @@ let glob_const_nvar loc env qid =
       | VarRef sp when
 	  Environ.evaluable_named_decl (Global.env ()) (basename sp) ->
 	  EvalVarRef (basename sp)
-      | _ -> error ((string_of_qualid qid) ^
+      | _ -> error ((Nametab.string_of_qualid qid) ^
 		    " does not denote an evaluable constant")
   with Not_found ->
-    Pretype_errors.error_global_not_found_loc loc qid
+    Nametab.error_global_not_found_loc loc qid
 
 let qid_interp = function
   | Node (loc, "QUALIDARG", p) -> interp_qualid p
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e2e719a1d1..72a371267e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -267,7 +267,7 @@ let add_resolves env sigma clist dbnames =
 
 let global qid =
   try Nametab.locate qid
-  with Not_found -> Pretype_errors.error_global_not_found_loc dummy_loc qid
+  with Not_found -> Nametab.error_global_not_found_loc dummy_loc qid
 
 (* REM : in most cases hintname = id *)
 let make_unfold (hintname, ref) =
@@ -387,7 +387,7 @@ let _ =
 			     | _ -> bad_vernac_args "HintConstructors") l in
     	       fun () -> add_resolves env sigma lcons dbnames
 	     with Invalid_argument("mind_specif_of_mind") -> 
-	       error ((string_of_qualid qid) ^ " is not an inductive type")
+	       error ((Nametab.string_of_qualid qid) ^ " is not an inductive type")
 	   end 
        | _ -> bad_vernac_args "HintConstructors")
     
@@ -420,7 +420,7 @@ let _ =
 		      let c = Declare.constr_of_reference Evd.empty env ref in
 		      let hyps = Declare.implicit_section_args ref in
 		      let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
-		      let _,i = repr_qualid qid in
+		      let _,i = Nametab.repr_qualid qid in
 		      (i, applist (c,section_args))
 		  | _-> bad_vernac_args "HintsResolve") lh in
 	   let dbnames = if l = [] then ["core"] else 
@@ -437,7 +437,7 @@ let _ =
 	   let lhints = 
 	     List.map (function
 			 | VARG_QUALID qid ->
-			     let _,n = repr_qualid qid in
+			     let _,n = Nametab.repr_qualid qid in
 			     (n, global qid)
 		      	 | _ -> bad_vernac_args "HintsUnfold") lh in
 	   let dbnames = if l = [] then ["core"] else 
@@ -456,7 +456,7 @@ let _ =
 	     List.map
 	       (function
 		  | VARG_QUALID qid -> 
-		      let _,n = repr_qualid qid in
+		      let _,n = Nametab.repr_qualid qid in
 		      let ref = Nametab.locate qid in
 		      let env = Global.env () in
 		      let c = Declare.constr_of_reference Evd.empty env ref in
@@ -954,8 +954,8 @@ let cvt_autoArgs =
        | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "String expected" >])
 
 let interp_to_add gl = function
-  | (Qualid qid) ->
-      let _,id = repr_qualid qid in
+  | Qualid qid ->
+      let _,id = Nametab.repr_qualid qid in
       (next_ident_away id (pf_ids_of_hyps gl), 
        Declare.constr_of_reference Evd.empty (Global.env()) (global qid))
   | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5fce67d510..4d1a2e2adc 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 cde9421d03..f04e99e79c 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 f87a5b2137..4a9c134f95 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 d0eb926a45..d95e254c88 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 fc4ef2968a..08fb2800d5 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 49042811a0..11e65b9349 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 5efd2bd40a..f1a93824cd 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 a6538bc1b1..e4595244ab 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 0c136820a7..5863ffb7b4 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