Removing the use of leveled tactics wit_tacticn. It is now handled

through a unique generic argument, and the level is only considered
at parsing time.

This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.

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

4 files changed, 25 insertions, 83 deletions

diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
deleted file mode 100644
index c20f43bd5..000000000
--- a/parsing/extrawit.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Genarg
-
-(* This file defines extra argument types *)
-
-(* Tactics as arguments *)
-
-let tactic_main_level = 5
-
-let wit_tactic0 = create_arg None "tactic0"
-let wit_tactic1 = create_arg None "tactic1"
-let wit_tactic2 = create_arg None "tactic2"
-let wit_tactic3 = create_arg None "tactic3"
-let wit_tactic4 = create_arg None "tactic4"
-let wit_tactic5 = create_arg None "tactic5"
-
-let wit_tactic = function
-  | 0 -> wit_tactic0
-  | 1 -> wit_tactic1
-  | 2 -> wit_tactic2
-  | 3 -> wit_tactic3
-  | 4 -> wit_tactic4
-  | 5 -> wit_tactic5
-  | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
-
-let tactic_genarg_level s =
-  if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
-    let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
-    else None
-  else None
-
-let () =
-  for i = 0 to 5 do
-    let name = Printf.sprintf "Extrawit.wit_tactic%i" i in
-    Genarg.register_name0 (wit_tactic i) name
-  done
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
deleted file mode 100644
index 1bd5cdb89..000000000
--- a/parsing/extrawit.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Genarg
-open Tacexpr
-
-(** This file defines extra argument types *)
-
-(** Tactics as arguments *)
-
-val tactic_main_level : int
-
-val wit_tactic : int -> (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-
-val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-
-val tactic_genarg_level : string -> int option
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2f0851164..500d7dde9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
 Tok
 Compat
 Lexer
-Extrawit
 Pcoq
 Egramml
 Egramcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2769612d5..211bf2632 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -16,7 +16,6 @@ open Genarg
 open Stdarg
 open Constrarg
 open Tacexpr
-open Extrawit
 
 (** The parser of Coq *)
 
@@ -398,7 +397,7 @@ module Tactic =
     let tactic_expr = Gram.entry_create "tactic:tactic_expr"
     let binder_tactic = Gram.entry_create "tactic:binder_tactic"
 
-    let tactic = make_gen_entry utactic (rawwit (wit_tactic tactic_main_level)) "tactic"
+    let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
 
     (* Main entry for quotations *)
     let tactic_eoi = eoi_entry tactic
@@ -756,6 +755,15 @@ let coincide s pat off =
   done;
   !break
 
+let tactic_level s =
+  if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
+    let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
+    else None
+  else None
+
+let type_of_entry u s =
+  type_of_typed_entry (get_entry u s)
+
 let rec interp_entry_name static up_level s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
@@ -784,20 +792,26 @@ let rec interp_entry_name static up_level s sep =
     | Some m -> Int.equal m n && not (Int.equal m 5)
     in
     let t, se =
-      match Extrawit.tactic_genarg_level s with
-	| Some n when check_lvl n -> None, Aself
-	| Some n when check_lvl (n + 1) -> None, Anext
-	| Some n -> None, Atactic n
-	| None ->
-      try Some (get_entry uprim s), Aentry ("prim",s) with Not_found ->
-      try Some (get_entry uconstr s), Aentry ("constr",s) with Not_found ->
-      try Some (get_entry utactic s), Aentry ("tactic",s) with Not_found ->
+      match tactic_level s with
+      | Some n ->
+        (** Quite ad-hoc *)
+        let t = unquote (rawwit wit_tactic) in
+        let se =
+          if check_lvl n then Aself
+          else if check_lvl (n + 1) then Anext
+          else Atactic n
+        in
+        (Some t, se)
+      | None ->
+      try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
+      try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
+      try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
 	if static then
 	  error ("Unknown entry "^s^".")
 	else
 	  None, Aentry ("",s) in
     let t =
       match t with
-	| Some t -> type_of_typed_entry t
+	| Some t -> t
 	| None -> ExtraArgType s in
     t, se