Changing the toplevel type of the int_or_var generic type to int.

7 files changed, 12 insertions, 31 deletions

diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index ef1ef4aee4..f2f314eea0 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 (** {5 Additional generic arguments} *)
 
-val wit_int_or_var : int or_var uniform_genarg_type
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
 val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 62f0ae5037..3c46e1eea0 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -21,12 +21,8 @@ open Misctypes
 
 DECLARE PLUGIN "micromega_plugin"
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z (out_arg i)) ]
+| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z i) ]
 | [ "psatz_Z" ] -> [  (Coq_micromega.psatz_Z (-1)) ]
 END
 
@@ -63,12 +59,12 @@ TACTIC EXTEND LRA_R
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R (out_arg i)) ]
+| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R i) ]
 | [ "psatz_R" ] -> [   (Coq_micromega.psatz_R (-1)) ]
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q (out_arg i)) ]
+| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q i) ]
 | [ "psatz_Q" ] -> [  (Coq_micromega.psatz_Q (-1)) ]
 END
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b511300758..94cbc54e94 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -337,7 +337,7 @@ module Make
 
   let rec pr_top_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
+      | IntOrVarArgType -> int (out_gen (topwit wit_int_or_var) x)
       | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
       | VarArgType -> pr_id (out_gen (topwit wit_var) x)
       | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 92d4960a7c..1b1fb845e0 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -115,12 +115,10 @@ END
 TACTIC EXTEND constructor
   [ "constructor" ] -> [ Tactics.any_constructor false None ]
 | [ "constructor" int_or_var(i) ] -> [
-    let i = Tacinterp.interp_int_or_var ist i in
     Tactics.constructor_tac false None i NoBindings
   ]
 | [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma; it = bl } = bl in
-    let i = Tacinterp.interp_int_or_var ist i in
     let tac = Tactics.constructor_tac false None i bl in
     Tacticals.New.tclWITHHOLES false tac sigma
   ]
@@ -129,12 +127,10 @@ END
 TACTIC EXTEND econstructor
   [ "econstructor" ] -> [ Tactics.any_constructor true None ]
 | [ "econstructor" int_or_var(i) ] -> [
-    let i = Tacinterp.interp_int_or_var ist i in
     Tactics.constructor_tac true None i NoBindings
   ]
 | [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma; it = bl } = bl in
-    let i = Tacinterp.interp_int_or_var ist i in
     let tac = Tactics.constructor_tac true None i bl in
     Tacticals.New.tclWITHHOLES true tac sigma
   ]
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2241fb821c..ffde67e4fb 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -104,11 +104,6 @@ let out_term = function
 
 let prolog_tac l n gl =
   let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
-  let n =
-    match n with
-      | ArgArg n -> n
-      | _ -> error "Prolog called with a non closed argument."
-  in
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" (str "Prolog failed.")
@@ -436,13 +431,11 @@ let gen_eauto ?(debug=Off) np lems = function
 
 let make_depth = function
   | None -> !default_search_depth
-  | Some (ArgArg d) -> d
-  | _ -> error "eauto called with a non closed argument."
+  | Some d -> d
 
 let make_dimension n = function
   | None -> (true,make_depth n)
-  | Some (ArgArg d) -> (false,d)
-  | _ -> error "eauto called with a non closed argument."
+  | Some d -> (false,d)
 
 open Genarg
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 92682fc7a0..4ddf9c1162 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -622,10 +622,6 @@ let subst_hole_with_term occ tc t =
 
 open Tacmach
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
 let hResolve id c occ t =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
@@ -664,7 +660,7 @@ let hResolve_auto id c t =
   resolve_auto 1
 
 TACTIC EXTEND hresolve_core
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c (out_arg occ) t ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c occ t ]
 | [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ]
 END
 
@@ -686,7 +682,7 @@ let hget_evar n =
   end }
 
 TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ]
+| [ "hget_evar" int_or_var(n) ] -> [ hget_evar n ]
 END
 
 (**********************************************************************)
@@ -909,12 +905,12 @@ END
 
 (* cycles [n] goals *)
 TACTIC EXTEND cycle
-| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ]
+| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle n ]
 END
 
 (* swaps goals number [i] and [j] *)
 TACTIC EXTEND swap
-| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap (out_arg i) (out_arg j) ]
+| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap i j ]
 END
 
 (* reverses the list of focused goals *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f87dc663bc..5a6834ab5d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1640,7 +1640,7 @@ and interp_genarg ist env sigma concl gl x =
     match genarg_tag x with
     | IntOrVarArgType ->
       in_gen (topwit wit_int_or_var)
-        (ArgArg (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x)))
+        (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x))
     | IdentArgType ->
       in_gen (topwit wit_ident)
         (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))