aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/mlutil.ml6
-rw-r--r--plugins/ltac/coretactics.mlg8
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_auto.mlg20
-rw-r--r--plugins/ltac/g_class.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg4
-rw-r--r--plugins/ltac/g_tactic.mlg6
-rw-r--r--plugins/ltac/pltac.ml2
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml9
-rw-r--r--plugins/ltac/tacinterp.ml9
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--plugins/micromega/g_micromega.mlg6
-rw-r--r--plugins/ssr/ssrparser.mlg2
17 files changed, 54 insertions, 44 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 21ec80abbc..da4a50b674 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
| MLuint i1, MLuint i2 -> Uint63.equal i1 i2
| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
-| _, _ -> false
+| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2
+| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _
+ |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom
+ | MLmagic _| MLuint _| MLfloat _|MLparray _), _
+ -> false
and eq_ml_pattern p1 p2 = match p1, p2 with
| Pcons (gr1, p1), Pcons (gr2, p2) ->
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index b7ac71181a..e39c066c95 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -122,10 +122,10 @@ END
TACTIC EXTEND constructor
| [ "constructor" ] -> { Tactics.any_constructor false None }
-| [ "constructor" int_or_var(i) ] -> {
+| [ "constructor" nat_or_var(i) ] -> {
Tactics.constructor_tac false None i NoBindings
}
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "constructor" nat_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac false None i bl in
Tacticals.New.tclDELAYEDWITHHOLES false bl tac
}
@@ -133,10 +133,10 @@ END
TACTIC EXTEND econstructor
| [ "econstructor" ] -> { Tactics.any_constructor true None }
-| [ "econstructor" int_or_var(i) ] -> {
+| [ "econstructor" nat_or_var(i) ] -> {
Tactics.constructor_tac true None i NoBindings
}
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "econstructor" nat_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac true None i bl in
Tacticals.New.tclDELAYEDWITHHOLES true bl tac
}
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index a2a47c0bf4..6ab82b1253 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -686,7 +686,7 @@ let hResolve_auto id c t =
}
TACTIC EXTEND hresolve_core
-| [ "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) ")" "at" nat_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
@@ -695,7 +695,7 @@ END
*)
TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n }
+| [ "hget_evar" nat_or_var(n) ] -> { Evar_tactics.hget_evar n }
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7e8400910c..eed9419946 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -96,17 +96,17 @@ TACTIC EXTEND debug_trivial
END
TACTIC EXTEND auto
-| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_auto
-| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "info_auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND debug_auto
-| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "debug" "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db }
END
@@ -130,15 +130,15 @@ let deprecated_bfs tacname =
}
TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
-TACTIC EXTEND new_eauto
-| [ "new" "auto" int_or_var_opt(n) auto_using(lems)
+TACTIC EXTEND new_eauto (* todo: name doesn't match syntax *)
+| [ "new" "auto" nat_or_var_opt(n) auto_using(lems)
hintbases(db) ] ->
{ match db with
| None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems)
@@ -146,7 +146,7 @@ TACTIC EXTEND new_eauto
END
TACTIC EXTEND debug_eauto
-| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "debug" "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
@@ -154,7 +154,7 @@ TACTIC EXTEND debug_eauto
END
TACTIC EXTEND info_eauto
-| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "info_eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
@@ -162,13 +162,13 @@ TACTIC EXTEND info_eauto
END
TACTIC EXTEND dfs_eauto
-| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "dfs" "eauto" nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND bfs_eauto
-| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "bfs" "eauto" nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{ Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
END
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8c2e633be5..0f59ac07b4 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -86,13 +86,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d ~strategy:Bfs l }
- | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
- | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c2e95c45f9..b1b96ea9a7 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -112,8 +112,8 @@ GRAMMAR EXTEND Gram
| true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
[ IDENT "try"; ta = ltac_expr -> { TacTry ta }
- | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
- | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+ | IDENT "do"; n = nat_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+ | IDENT "timeout"; n = nat_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
| IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
| IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
| IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 072206c39c..43957bbde5 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -190,7 +190,7 @@ open Pvernac.Vernac_
GRAMMAR EXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
- bindings red_expr int_or_var open_constr uconstr
+ bindings red_expr int_or_var nat_or_var open_constr uconstr
simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
int_or_var:
@@ -407,8 +407,8 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
- | -> { None } ] ]
+ [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
+ | -> { [] } ] ]
;
orient_rw:
[ [ "->" -> { true }
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 94e398fe5d..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -29,6 +29,7 @@ let quantified_hypothesis =
Entry.create "quantified_hypothesis"
let destruction_arg = Entry.create "destruction_arg"
let int_or_var = Entry.create "int_or_var"
+let nat_or_var = Entry.create "nat_or_var"
let simple_intropattern =
Entry.create "simple_intropattern"
let in_clause = Entry.create "in_clause"
@@ -52,6 +53,7 @@ let () =
let open Stdarg in
let open Tacarg in
register_grammar wit_int_or_var (int_or_var);
+ register_grammar wit_nat_or_var (nat_or_var);
register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *)
(* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *)
register_grammar wit_simple_intropattern (simple_intropattern);
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 3a4a081c93..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -27,6 +27,7 @@ val uconstr : constr_expr Entry.t
val quantified_hypothesis : quantified_hypothesis Entry.t
val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
val int_or_var : int Locus.or_var Entry.t
+val nat_or_var : int Locus.or_var Entry.t
val simple_tactic : raw_tactic_expr Entry.t
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
val in_clause : Names.lident Locus.clause_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index edd56ee0f7..cd7b1f7f28 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -458,8 +458,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
let pr_in_hyp_as prc pr_id = function
- | None -> mt ()
- | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+ | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
let pr_in_clause pr_id = function
| { onhyps=None; concl_occs=NoOccurrences } ->
@@ -756,7 +755,7 @@ let pr_goal_selector ~toplevel s =
(if a then mt() else primitive "simple ") ++
primitive (with_evars ev "apply") ++ spc () ++
prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+ prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
)
| TacElim (ev,cb,cbo) ->
hov 1 (
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index eaedf8d9c1..7b2c8e1d04 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -108,7 +108,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 50767821e4..2382dcfbb9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -107,7 +107,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 47f1d3bf66..8bee7afa2c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -444,11 +444,11 @@ let intern_red_expr ist = function
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
-let intern_in_hyp_as ist lf (id,ipat) =
- (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
let intern_hyp_list ist = List.map (intern_hyp ist)
+let intern_in_hyp_as ist lf (idl,ipat) =
+ (intern_hyp ist idl, Option.map (intern_intro_pattern lf ist) ipat)
+
let intern_inversion_strength lf ist = function
| NonDepInversion (k,idl,ids) ->
NonDepInversion (k,intern_hyp_list ist idl,
@@ -527,7 +527,7 @@ let rec intern_atomic lf ist x =
TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
| TacApply (a,ev,cb,inhyp) ->
TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
- Option.map (intern_in_hyp_as ist lf) inhyp)
+ List.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings_arg ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
@@ -799,6 +799,7 @@ let intern_ltac ist tac =
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+ Genintern.register_intern0 wit_nat_or_var (lift intern_int_or_var);
Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3d734d3a66..00ac155f0e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
(k,(make ?loc f))) cb
in
let sigma,tac = match cl with
- | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
- | Some cl ->
- let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
- sigma, Tactics.apply_delayed_in a ev id l cl in
+ | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
+ | cl ->
+ let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in
+ sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in
Tacticals.New.tclWITHHOLES ev tac sigma
end
end
@@ -2099,6 +2099,7 @@ let interp_pre_ident ist env sigma s =
let () =
register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+ register_interp0 wit_nat_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
register_interp0 wit_smart_global (lift interp_reference);
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ec44ae4698..90546ea939 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -128,7 +128,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Basic tactics *)
| TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
| TacApply (a,ev,cb,cl) ->
- TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
+ TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,
+ List.map (on_snd (Option.map (subst_intro_pattern subst))) cl)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_glob_with_bindings_arg subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
@@ -278,6 +279,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
let () =
Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
+ Genintern.register_subst0 wit_nat_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg
index 40eea91b31..852a485329 100644
--- a/plugins/micromega/g_micromega.mlg
+++ b/plugins/micromega/g_micromega.mlg
@@ -29,7 +29,7 @@ open Tacarg
DECLARE PLUGIN "micromega_plugin"
TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
+| [ "psatz_Z" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
(Tacinterp.tactic_of_value ist t))
}
| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
@@ -74,12 +74,12 @@ TACTIC EXTEND LRA_R
END
TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
END
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index ccdf5fa68e..f06b460ee9 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1792,7 +1792,7 @@ GRAMMAR EXTEND Gram
{ ssrdotac_expr ~loc noindex m tac clauses }
| IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
{ ssrdotac_expr ~loc noindex Once tac clauses }
- | IDENT "do"; n = int_or_var; m = ssrmmod;
+ | IDENT "do"; n = nat_or_var; m = ssrmmod;
tac = ssrdotac; clauses = ssrclauses ->
{ ssrdotac_expr ~loc (mk_index ~loc n) m tac clauses }
] ];
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 18:03:48 +0000