Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands

It is quite nasty to insert those open in places where they can change
the semantics of surrounding code... instead, prefer using
fully-qualified names in generated code when possible. For
ExtraArgType, simulate a "open Extrawit in ..." (which does exist
primitively in OCaml >= 3.12) with the usual encoding.

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

3 files changed, 36 insertions, 23 deletions

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index c95f7ed45d..d3f28b0570 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -189,11 +189,10 @@ END
 (** Fix a quotation difference in [str_item] *)
 
 let declare_str_items loc l =
-  let l' = <:str_item< open Pcoq >> :: <:str_item< open Extrawit >> :: l in
 IFDEF CAMLP5 THEN
-  MLast.StDcl (loc,l') (* correspond to <:str_item< declare $list:l'$ end >> *)
+  MLast.StDcl (loc,l) (* correspond to <:str_item< declare $list:l'$ end >> *)
 ELSE
-  Ast.stSem_of_list l'
+  Ast.stSem_of_list l
 END
 
 (** Quotation difference for match clauses *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index dd4f2eb051..90116180eb 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -40,7 +40,12 @@ let rec make_rawwit loc = function
   | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
   | PairArgType (t1,t2) ->
       <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >>
-  | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >>
+  | ExtraArgType s ->
+    <:expr<
+      let module WIT = struct
+        open Extrawit;
+        value wit = $lid:"rawwit_"^s$;
+      end in WIT.wit >>
 
 let rec make_globwit loc = function
   | BoolArgType -> <:expr< Genarg.globwit_bool >>
@@ -65,7 +70,12 @@ let rec make_globwit loc = function
   | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >>
   | PairArgType (t1,t2) ->
       <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >>
-  | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >>
+  | ExtraArgType s ->
+    <:expr<
+      let module WIT = struct
+        open Extrawit;
+        value wit = $lid:"globwit_"^s$;
+      end in WIT.wit >>
 
 let rec make_wit loc = function
   | BoolArgType -> <:expr< Genarg.wit_bool >>
@@ -90,24 +100,29 @@ let rec make_wit loc = function
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
   | PairArgType (t1,t2) ->
       <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
-  | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >>
+  | ExtraArgType s ->
+    <:expr<
+      let module WIT = struct
+        open Extrawit;
+        value wit = $lid:"wit_"^s$;
+      end in WIT.wit >>
 
 let make_act loc act pil =
   let rec make = function
-    | [] -> <:expr< Gram.action (fun loc -> ($act$ : 'a)) >>
+    | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
     | GramNonTerminal (_,t,_,Some p) :: tl ->
 	let p = Names.string_of_id p in
 	<:expr<
-          Gram.action
+          Pcoq.Gram.action
             (fun $lid:p$ ->
                let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
         >>
     | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl ->
-	<:expr< Gram.action (fun _ -> $make tl$) >> in
+	<:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in
   make (List.rev pil)
 
 let make_prod_item = function
-  | GramTerminal s -> <:expr< gram_token_of_string $str:s$ >>
+  | GramTerminal s -> <:expr< Pcoq.gram_token_of_string $str:s$ >>
   | GramNonTerminal (_,_,g,_) ->
       <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >>
 
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 3a30701155..91ab29f1d4 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -52,19 +52,18 @@ let mlexpr_of_option f = function
   | Some e -> <:expr< Some $f e$ >>
 
 open Vernacexpr
-open Pcoq
 open Genarg
 
 let rec mlexpr_of_prod_entry_key = function
-  | Alist1 s -> <:expr< Alist1 $mlexpr_of_prod_entry_key s$ >>
-  | Alist1sep (s,sep) -> <:expr< Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Alist0 s -> <:expr< Alist0 $mlexpr_of_prod_entry_key s$ >>
-  | Alist0sep (s,sep) -> <:expr< Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Aopt s -> <:expr< Aopt $mlexpr_of_prod_entry_key s$ >>
-  | Amodifiers s -> <:expr< Amodifiers $mlexpr_of_prod_entry_key s$ >>
-  | Aself -> <:expr< Aself >>
-  | Anext -> <:expr< Anext >>
-  | Atactic n -> <:expr< Atactic $mlexpr_of_int n$ >>
-  | Agram s -> Util.anomaly "Agram not supported"
-  | Aentry ("",s) -> <:expr< Agram (Gram.Entry.obj $lid:s$) >>
-  | Aentry (u,s) -> <:expr< Aentry $str:u$ $str:s$ >>
+  | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
+  | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
+  | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
+  | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
+  | Pcoq.Aself -> <:expr< Pcoq.Aself >>
+  | Pcoq.Anext -> <:expr< Pcoq.Anext >>
+  | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
+  | Pcoq.Agram s -> Util.anomaly "Agram not supported"
+  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >>
+  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>