From 3415801b2c368ce03f6e8d33a930b9ab9e0b9fd1 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 2 Oct 2012 15:57:25 +0000
Subject: Argextend: avoid useless "open Extrawit"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15843 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 grammar/argextend.ml4 | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 9f807f783..a02b7babc 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -17,6 +17,16 @@ open Compat
 let loc = Loc.ghost
 let default_loc = <:expr< Loc.ghost >>
 
+let mk_extraarg prefix s =
+  if Extrawit.tactic_genarg_level s = None then
+    <:expr< $lid:prefix^s$ >>
+  else
+    <:expr<
+      let module WIT = struct
+        open Extrawit;
+        value wit = $lid:prefix^s$;
+      end in WIT.wit >>
+
 let rec make_rawwit loc = function
   | BoolArgType -> <:expr< Genarg.rawwit_bool >>
   | IntArgType -> <:expr< Genarg.rawwit_int >>
@@ -40,12 +50,7 @@ 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<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"rawwit_"^s$;
-      end in WIT.wit >>
+  | ExtraArgType s -> mk_extraarg "rawwit_" s
 
 let rec make_globwit loc = function
   | BoolArgType -> <:expr< Genarg.globwit_bool >>
@@ -70,12 +75,7 @@ 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<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"globwit_"^s$;
-      end in WIT.wit >>
+  | ExtraArgType s ->  mk_extraarg "globwit_" s
 
 let rec make_wit loc = function
   | BoolArgType -> <:expr< Genarg.wit_bool >>
@@ -100,12 +100,7 @@ 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<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"wit_"^s$;
-      end in WIT.wit >>
+  | ExtraArgType s -> mk_extraarg "wit_" s
 
 let has_extraarg =
   List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
-- 
cgit v1.2.3