From 89abe2a141b3baa11bf0e8bcdecaf68220251c6e Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 2 Jul 2013 14:46:47 +0000
Subject: Removed the ad-hod handling of wit_tacticn.

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

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index eb4630394b..dfcaa4e84c 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -22,14 +22,11 @@ let qualified_name loc s =
   qualified_name loc path name
 
 let mk_extraarg loc s =
-  if Extrawit.tactic_genarg_level s = None then
-    try
-      let name = Genarg.get_name0 s in
-      qualified_name loc name
-    with Not_found ->
-      <:expr< $lid:"wit_"^s$ >>
-  else
-    qualified_name loc ("Extrawit.wit_" ^ s)
+  try
+    let name = Genarg.get_name0 s in
+    qualified_name loc name
+  with Not_found ->
+    <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
-- 
cgit v1.2.3