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

15 files changed, 52 insertions, 129 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 3a8a2cc3d..c3d3ce709 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -155,7 +155,6 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
-Extrawit
 Pcoq
 Printer
 Pptactic
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index f361bee49..bde5c15f3 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -31,7 +31,6 @@ Stdarg
 Constrarg
 Tok
 Lexer
-Extrawit
 Pcoq
 Q_util
 Q_coqast
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 1b29da681..d494a92d8 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -15,7 +15,6 @@ open Q_util
 open Q_coqast
 open Argextend
 open Pcoq
-open Extrawit
 open Egramml
 open Compat
 
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 87da56e4f..5c2b3392c 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -14,6 +14,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Genredexpr
+open Tacexpr
 open Pattern
 open Constrexpr
 open Term
@@ -35,6 +36,9 @@ let wit_int_or_var = unsafe_of_type IntOrVarArgType
 let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
   Genarg.make0 None "intropattern"
 
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
+  Genarg.make0 None "tactic"
+
 let wit_ident_gen b = unsafe_of_type (IdentArgType b)
 
 let wit_ident = wit_ident_gen true
@@ -69,4 +73,6 @@ let wit_red_expr = unsafe_of_type RedExprArgType
 
 (** Register location *)
 
-let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"
+let () =
+  register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
+  register_name0 wit_tactic "Constrarg.wit_tactic"
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 548bd6690..1233e165f 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -77,3 +77,5 @@ val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
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
diff --git a/printing/ppextra.ml b/printing/ppextra.ml
deleted file mode 100644
index 8acdd2e1b..000000000
--- a/printing/ppextra.ml
+++ /dev/null
@@ -1,20 +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 Ppextend
-open Pptactic
-open Extrawit
-
-let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
-
-let _ = for i=0 to 5 do
-  let wit = wit_tactic i in
-  declare_extra_genarg_pprule wit
-    (pr_tac_polymorphic i) (pr_tac_polymorphic i) (pr_tac_polymorphic i)
-done
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3b3de2a3c..0fd3b454c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1011,6 +1011,10 @@ let register_uniform_printer wit pr =
 let () = Genprint.register_print0 Constrarg.wit_intro_pattern
   pr_intro_pattern pr_intro_pattern pr_intro_pattern
 
+let () =
+  let printer _ _ prtac = prtac (0, E) in
+  declare_extra_genarg_pprule wit_tactic printer printer printer
+
 let _ = Hook.set Tactic_debug.tactic_printer
   (fun x -> pr_glob_tactic (Global.env()) x)
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6d50c02e2..1a63ca2da 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -27,7 +27,6 @@ open Tacexpr
 open Genarg
 open Constrarg
 open Mod_subst
-open Extrawit
 open Misctypes
 open Locus
 
@@ -950,9 +949,7 @@ let () =
 
 let () =
   let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in
-  for i = 0 to 5 do
-    Genintern.register_intern0 (wit_tactic i) intern
-  done
+  Genintern.register_intern0 wit_tactic intern
 
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 67fa0ed7b..d5c48f9e6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -37,7 +37,6 @@ open Stdarg
 open Constrarg
 open Printer
 open Pretyping
-open Extrawit
 open Evd
 open Misctypes
 open Miscops
@@ -1910,13 +1909,6 @@ and interp_atomic ist gl tac =
         let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
 	evdref := sigma;
 	Value.of_constr c_interp
-    | ExtraArgType s when not (Option.is_empty (tactic_genarg_level s)) ->
-          (* Special treatment of tactic arguments *)
-	let (sigma,v) = val_interp ist gl
-          (out_gen (glbwit (wit_tactic (Option.get (tactic_genarg_level s)))) x)
-	in
-	evdref := sigma;
-	v
     | List0ArgType ConstrArgType ->
         let wit = glbwit (wit_list0 wit_constr) in
 	let (sigma,l_interp) =
@@ -1966,9 +1958,17 @@ and interp_atomic ist gl tac =
     | List0ArgType _ -> app_list0 f x
     | List1ArgType _ -> app_list1 f x
     | ExtraArgType _ ->
-      let (sigma, v) = Geninterp.generic_interp ist { gl with sigma = !evdref } x in
-      evdref := sigma;
-      v
+      (** Special treatment of tactics *)
+      let gl = { gl with sigma = !evdref } in
+      if has_type x (glbwit wit_tactic) then
+        let tac = out_gen (glbwit wit_tactic) x in
+        let (sigma, v) = val_interp ist gl tac in
+        let () = evdref := sigma in
+        v
+      else
+        let (sigma, v) = Geninterp.generic_interp ist gl x in
+        let () = evdref := sigma in
+        v
     | QuantHypArgType | RedExprArgType
     | OpenConstrArgType _ | ConstrWithBindingsArgType
     | BindingsArgType
@@ -2064,9 +2064,7 @@ let () =
     let f = VFun (extract_trace ist, ist.lfun, [], tac) in
     (gl.sigma, TacArg (dloc, valueIn (of_tacvalue f)))
   in
-  for i = 0 to 5 do
-    Geninterp.register_interp0 (wit_tactic i) interp
-  done
+  Geninterp.register_interp0 wit_tactic interp
 
 (***************************************************************************)
 (* Other entry points *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 006885616..11b747e72 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -329,8 +329,6 @@ and subst_genarg subst (x:glob_generic_argument) =
 let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
 
 let () =
-  for i = 0 to 5 do
-    Genintern.register_subst0 (Extrawit.wit_tactic i) subst_tactic
-  done
+  Genintern.register_subst0 wit_tactic subst_tactic
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index a3da105ae..b27c7588d 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -12,7 +12,6 @@ Obligations
 Command
 Classes
 Record
-Ppextra
 Ppvernac
 Backtrack
 Vernacinterp