Removing useless tactic arguments, and using generic arguments

instead (proof of concept, to be extended).

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

4 files changed, 16 insertions, 9 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index b1830523b..3f52de11c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -688,10 +688,10 @@ and intern_tactic_seq onlytac ist = function
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
-  | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a)
+  | TacCall _ | TacExternal _ | Reference _
+  | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | TacVoid | IntroPattern _ | Integer _
-  | ConstrMayEval _ | TacFreshId _ as a ->
+  | IntroPattern _ | ConstrMayEval _ | TacFreshId _ as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
   | MetaIdArg _ -> assert false
 
@@ -705,12 +705,10 @@ and intern_tactic_fun ist (var,body) =
   (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
 
 and intern_tacarg strict onlytac ist = function
-  | TacVoid -> TacVoid
   | Reference r -> intern_non_tactic_reference strict ist r
   | IntroPattern ipat ->
       let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
       IntroPattern (intern_intro_pattern lf ist ipat)
-  | Integer n -> Integer n
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
@@ -728,6 +726,9 @@ and intern_tacarg strict onlytac ist = function
       TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
   | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
   | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
+  | TacGeneric arg ->
+    let (_, arg) = Genintern.generic_intern ist arg in
+    TacGeneric arg
   | TacDynamic(loc,t) as x ->
       (match Dyn.tag t with
 	| "tactic" | "value" -> x
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 09dcb49f4..de72f2b5c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1090,12 +1090,15 @@ and interp_ltac_reference loc' mustbetac ist gl = function
 and interp_tacarg ist gl arg =
   let evdref = ref (project gl) in
   let v = match arg with
-    | TacVoid -> in_gen (topwit wit_unit) ()
+    | TacGeneric arg ->
+      let gl = { gl with sigma = !evdref } in
+      let (sigma, v) = Geninterp.generic_interp ist gl arg in
+      evdref := sigma;
+      v
     | Reference r ->
       let (sigma,v) = interp_ltac_reference dloc false ist gl r in
       evdref := sigma;
       v
-    | Integer n -> in_gen (topwit wit_int) n
     | IntroPattern ipat ->
       let ans = interp_intro_pattern ist gl ipat in
       in_gen (topwit wit_intro_pattern) ans
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index dcdaf9dbc..274c3b352 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -264,8 +264,9 @@ and subst_tacarg subst = function
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
   | TacExternal (_loc,com,req,la) ->
       TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
-  | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
+  | (IntroPattern _ | TacFreshId _) as x -> x
   | Tacexp t -> Tacexp (subst_tactic subst t)
+  | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
   | TacDynamic(the_loc,t) as x ->
       (match Dyn.tag t with
 	| "tactic" | "value" -> x
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ab31b664d..587ea3311 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -13,6 +13,8 @@ open Hipattern
 open Names
 open Globnames
 open Pp
+open Genarg
+open Stdarg
 open Tacticals
 open Tacinterp
 open Tactics
@@ -174,7 +176,7 @@ let flatten_contravariant_disj flags ist =
       let hyp = valueIn (Value.of_constr hyp) in
       iter_tac (List.map_i (fun i arg ->
 	let typ = valueIn (Value.of_constr (mkArrow arg c)) in
-	let i = Tacexpr.Integer i in
+	let i = Tacexpr.TacGeneric (in_gen (rawwit wit_int) i) in
 	<:tactic<
           let typ := $typ in
           let hyp := $hyp in