From f68ff500a9090da58f573ce68e4b8b080e871e28 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 19 Jun 2013 14:14:23 +0000
Subject: Fixing argument extension. Instead of qualified names, string
 representing qualified names where interpreted as a whole lowercase ident.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16593 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build        |  2 +-
 grammar/argextend.ml4 | 14 ++++++++------
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 0dda6140c..b68a02cf6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -68,7 +68,7 @@ ALLDEPS:=$(addsuffix .d, \
 VERBOSE=
 NO_RECOMPILE_ML4=
 NO_RECALC_DEPS=
-READABLE_ML4=1	# non-empty means .ml of .ml4 will be ascii instead of binary
+READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 4ea5f35c1..6fde4fafe 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -16,19 +16,21 @@ open Compat
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
 
+let qualified_name s =
+  let path = CString.split '.' s in
+  let (name, path) = CList.sep_last path in
+  let fold dir accu = <:expr< $uid:dir$.$accu$ >> in
+  List.fold_right fold path <:expr< $lid:name$ >>
+
 let mk_extraarg s =
   if Extrawit.tactic_genarg_level s = None then
     try
       let name = Genarg.get_name0 s in
-      <:expr< $lid:name$ >>
+      qualified_name name
     with Not_found ->
       <:expr< $lid:"wit_"^s$ >>
   else
-      <:expr<
-        let module WIT = struct
-          open Extrawit;
-          value wit = $lid:"wit_"^s$;
-        end in WIT.wit >>
+    qualified_name ("Extrawit.wit_" ^ s)
 
 let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
-- 
cgit v1.2.3