aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--dev/doc/parsing.md6
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst4
-rw-r--r--doc/tools/docgram/README.md2
-rw-r--r--doc/tools/docgram/common.edit_mlg125
-rw-r--r--doc/tools/docgram/fullGrammar124
-rw-r--r--lib/genarg.mli2
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg90
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/pltac.ml3
-rw-r--r--plugins/ltac/pltac.mli2
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacentries.ml8
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/ltac/tacinterp.mli4
-rw-r--r--plugins/ssr/ssrparser.mlg46
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
18 files changed, 213 insertions, 215 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 5e3199e8a6..83929bd030 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -469,7 +469,7 @@ let rec parse_symb self = function
| Uentryl (e, l) ->
assert (e = "tactic");
if l = 5 then SymbEntry ("Pltac.binder_tactic", None)
- else SymbEntry ("Pltac.tactic_expr", Some (string_of_int l))
+ else SymbEntry ("Pltac.ltac_expr", Some (string_of_int l))
let parse_token self = function
| ExtTerminal s -> (terminal s, None)
diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md
index 4982e3e94d..4956b91d01 100644
--- a/dev/doc/parsing.md
+++ b/dev/doc/parsing.md
@@ -210,7 +210,7 @@ command. The first square bracket around a nonterminal definition is for groupi
level definitions, which are separated with `|`, for example:
```
- tactic_expr:
+ ltac_expr:
[ "5" RIGHTA
[ te = binder_tactic -> { te } ]
| "4" LEFTA
@@ -220,8 +220,8 @@ level definitions, which are separated with `|`, for example:
Grammar extensions can specify what level they are modifying, for example:
```
- tactic_expr: LEVEL "1" [ RIGHTA
- [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+ ltac_expr: LEVEL "1" [ RIGHTA
+ [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
```
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 94a705a4c6..fc5aa3f93d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -477,10 +477,10 @@ Displaying information about notations
such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level.
For example, this output from `Print Grammar tactic` shows the first 3 levels for
- `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative,
+ `ltac_expr`, designated as "5", "4" and "3". Level 3 is right-associative,
which applies to the productions within it, such as the `try` construct::
- Entry tactic_expr is
+ Entry ltac_expr is
[ "5" RIGHTA
[ binder_tactic ]
| "4" LEFTA
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 4d38955fa8..dbb04bb6a6 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -42,7 +42,7 @@ for documentation purposes:
First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example:
```
- tactic_expr:
+ ltac_expr:
[ "5" RIGHTA
[ te = binder_tactic -> { te } ]
[ "4" ...
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 36b20c0920..1e4101db1c 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -29,7 +29,7 @@ strategy_level_or_var: [
]
term0: [
-| "ltac" ":" "(" tactic_expr5 ")"
+| "ltac" ":" "(" ltac_expr5 ")"
]
EXTRAARGS_natural: [ | DELETENT ]
@@ -183,19 +183,19 @@ DELETE: [
(* additional nts to be spliced *)
tactic_then_last: [
-| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
-| WITH LIST0 ( "|" ( OPT tactic_expr5 ) )
+| REPLACE "|" LIST0 ( OPT ltac_expr5 ) SEP "|"
+| WITH LIST0 ( "|" ( OPT ltac_expr5 ) )
]
goal_tactics: [
-| LIST0 ( OPT tactic_expr5 ) SEP "|"
+| LIST0 ( OPT ltac_expr5 ) SEP "|"
]
tactic_then_gen: [ | DELETENT ]
tactic_then_gen: [
| goal_tactics
-| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics )
+| OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics )
]
tactic_then_last: [
@@ -308,7 +308,7 @@ atomic_constr: [
| MOVETO term_evar pattern_ident evar_instance
]
-tactic_expr0: [
+ltac_expr0: [
| REPLACE "[" ">" tactic_then_gen "]"
| WITH "[>" tactic_then_gen "]"
]
@@ -396,7 +396,7 @@ term0: [
| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
| MOVETO term_generalizing "`{" term200 "}"
| MOVETO term_generalizing "`(" term200 ")"
-| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
+| MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")"
| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
]
@@ -822,67 +822,67 @@ DELETE: [
| tactic_then_locality
]
-tactic_expr5: [
-(* make these look consistent with use of binder_tactic in other tactic_expr* *)
+ltac_expr5: [
+(* make these look consistent with use of binder_tactic in other ltac_expr* *)
| DELETE binder_tactic
-| DELETE tactic_expr4
-| [ tactic_expr4 | binder_tactic ]
+| DELETE ltac_expr4
+| [ ltac_expr4 | binder_tactic ]
]
ltac_constructs: [
(* repeated in main ltac grammar - need to create a COPY edit *)
-| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
-| tactic_expr3 ";" "[" tactic_then_gen "]"
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" tactic_then_gen "]"
-| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ]
-| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
(* | qualid LIST0 tactic_arg add later due renaming tactic_arg *)
| "[>" tactic_then_gen "]"
-| toplevel_selector tactic_expr5
+| toplevel_selector ltac_expr5
]
-tactic_expr4: [
-| REPLACE tactic_expr3 ";" tactic_then_gen "]"
-| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
-| REPLACE tactic_expr3 ";" binder_tactic
-| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
-| DELETE tactic_expr3 ";" tactic_expr3
+ltac_expr4: [
+| REPLACE ltac_expr3 ";" tactic_then_gen "]"
+| WITH ltac_expr3 ";" "[" tactic_then_gen "]"
+| REPLACE ltac_expr3 ";" binder_tactic
+| WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| DELETE ltac_expr3 ";" ltac_expr3
]
l3_tactic: [ ]
-tactic_expr3: [
-| DELETE "abstract" tactic_expr2
-| REPLACE "abstract" tactic_expr2 "using" ident
-| WITH "abstract" tactic_expr2 OPT ( "using" ident )
+ltac_expr3: [
+| DELETE "abstract" ltac_expr2
+| REPLACE "abstract" ltac_expr2 "using" ident
+| WITH "abstract" ltac_expr2 OPT ( "using" ident )
| l3_tactic
| MOVEALLBUT ltac_builtins
| l3_tactic
-| tactic_expr2
+| ltac_expr2
]
l2_tactic: [ ]
-tactic_expr2: [
-| REPLACE tactic_expr1 "+" binder_tactic
-| WITH tactic_expr1 "+" [ tactic_expr2 | binder_tactic ]
-| DELETE tactic_expr1 "+" tactic_expr2
-| REPLACE tactic_expr1 "||" binder_tactic
-| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
-| DELETE tactic_expr1 "||" tactic_expr2
-| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
+ltac_expr2: [
+| REPLACE ltac_expr1 "+" binder_tactic
+| WITH ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| DELETE ltac_expr1 "+" ltac_expr2
+| REPLACE ltac_expr1 "||" binder_tactic
+| WITH ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| DELETE ltac_expr1 "||" ltac_expr2
+| MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
| l2_tactic
| DELETE ltac_builtins
]
l1_tactic: [ ]
-tactic_expr1: [
+ltac_expr1: [
| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
| MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
-| MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end"
+| MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end"
| REPLACE failkw [ int_or_var | ] LIST0 message_token
| WITH failkw OPT int_or_var LIST0 message_token
| REPLACE reference LIST0 tactic_arg_compat
@@ -893,7 +893,7 @@ tactic_expr1: [
| l1_tactic
| tactic_arg
| reference LIST1 tactic_arg_compat
-| tactic_expr0
+| ltac_expr0
]
(* split match_context_rule *)
@@ -904,10 +904,10 @@ goal_pattern: [
]
match_context_rule: [
-| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
-| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
-| DELETE "_" "=>" tactic_expr5
-| goal_pattern "=>" tactic_expr5
+| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" ltac_expr5
+| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" ltac_expr5
+| DELETE "_" "=>" ltac_expr5
+| goal_pattern "=>" ltac_expr5
]
match_context_list: [
@@ -920,7 +920,7 @@ match_list: [
match_rule: [
(* redundant; match_pattern -> term -> _ *)
-| DELETE "_" "=>" tactic_expr5
+| DELETE "_" "=>" ltac_expr5
]
selector_body: [
@@ -1102,10 +1102,10 @@ simple_tactic: [
| REPLACE "show" "ltac" "profile" "cutoff" integer
| WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
| DELETE "show" "ltac" "profile" string
-(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
+(* perversely, the mlg uses "tactic3" instead of "ltac_expr3" *)
| DELETE "transparent_abstract" tactic3
| REPLACE "transparent_abstract" tactic3 "using" ident
-| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident )
+| WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident )
| REPLACE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
| WITH "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident )
| DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
@@ -1113,7 +1113,7 @@ simple_tactic: [
| DELETE "typeclasses" "eauto" OPT int_or_var
(* in Tactic Notation: *)
| "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp )
- OPT ( "at" LIST1 int_or_var ) OPT ( "by" tactic_expr3 )
+ OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
]
(* todo: don't use DELETENT for this *)
@@ -1372,8 +1372,8 @@ numnotoption: [
]
binder_tactic: [
-| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
-| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
+| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
| MOVEALLBUT ltac_builtins
]
@@ -1813,9 +1813,9 @@ input_fun: [
]
let_clause: [
-| DELETE identref ":=" tactic_expr5
-| REPLACE "_" ":=" tactic_expr5
-| WITH name ":=" tactic_expr5
+| DELETE identref ":=" ltac_expr5
+| REPLACE "_" ":=" ltac_expr5
+| WITH name ":=" ltac_expr5
]
tactic_mode: [
@@ -1900,7 +1900,7 @@ query_command: [ ] (* re-add as a placeholder *)
sentence: [
| OPT attributes command "."
| OPT attributes OPT ( natural ":" ) query_command "."
-| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
+| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr5 [ "." | "..." ]
| control_command
]
@@ -1924,18 +1924,18 @@ ltac_defined_tactics: [
| "split_Rabs"
| "split_Rmult"
| "tauto"
-| "time_constr" tactic_expr5
+| "time_constr" ltac_expr5
| "zify"
]
(* todo: need careful review; assume that "[" ... "]" are literals *)
tactic_notation_tactics: [
-| "assert_fails" tactic_expr3
-| "assert_succeeds" tactic_expr3
+| "assert_fails" ltac_expr3
+| "assert_succeeds" ltac_expr3
| "field" OPT ( "[" LIST1 constr "]" )
| "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
| "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
-| "intuition" OPT tactic_expr5
+| "intuition" OPT ltac_expr5
| "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
| "psatz" constr OPT int_or_var
| "ring" OPT ( "[" LIST1 constr "]" )
@@ -1987,9 +1987,9 @@ simple_tactic: [
]
tacdef_body: [
-| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5
-| WITH global LIST0 input_fun ltac_def_kind tactic_expr5
-| DELETE global ltac_def_kind tactic_expr5
+| REPLACE global LIST1 input_fun ltac_def_kind ltac_expr5
+| WITH global LIST0 input_fun ltac_def_kind ltac_expr5
+| DELETE global ltac_def_kind ltac_expr5
]
tac2def_typ: [
@@ -2490,12 +2490,7 @@ RENAME: [
| tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *)
| tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *)
| ltac1_expr ltac_expr
-| tactic_expr5 ltac_expr
-| tactic_expr4 ltac_expr4
-| tactic_expr3 ltac_expr3
-| tactic_expr2 ltac_expr2
-| tactic_expr1 ltac_expr1
-| tactic_expr0 ltac_expr0
+| ltac_expr5 ltac_expr
(* | nonsimple_intropattern intropattern (* ltac2 *) *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 9a2e4cd8e7..538ab8947c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1925,15 +1925,15 @@ eauto_search_strategy: [
]
tactic_then_last: [
-| "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
+| "|" LIST0 ( OPT ltac_expr5 ) SEP "|"
|
]
tactic_then_gen: [
-| tactic_expr5 "|" tactic_then_gen
-| tactic_expr5 ".." tactic_then_last
+| ltac_expr5 "|" tactic_then_gen
+| ltac_expr5 ".." tactic_then_last
| ".." tactic_then_last
-| tactic_expr5
+| ltac_expr5
| "|" tactic_then_gen
|
]
@@ -1942,59 +1942,59 @@ tactic_then_locality: [
| "[" OPT ">"
]
-tactic_expr5: [
+ltac_expr5: [
| binder_tactic
-| tactic_expr4
-]
-
-tactic_expr4: [
-| tactic_expr3 ";" binder_tactic
-| tactic_expr3 ";" tactic_expr3
-| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]"
-| tactic_expr3
-]
-
-tactic_expr3: [
-| "try" tactic_expr3
-| "do" int_or_var tactic_expr3
-| "timeout" int_or_var tactic_expr3
-| "time" OPT string tactic_expr3
-| "repeat" tactic_expr3
-| "progress" tactic_expr3
-| "once" tactic_expr3
-| "exactly_once" tactic_expr3
-| "infoH" tactic_expr3
-| "abstract" tactic_expr2
-| "abstract" tactic_expr2 "using" ident
-| selector tactic_expr3
-| tactic_expr2
-]
-
-tactic_expr2: [
-| tactic_expr1 "+" binder_tactic
-| tactic_expr1 "+" tactic_expr2
-| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
-| tactic_expr1 "||" binder_tactic
-| tactic_expr1 "||" tactic_expr2
-| tactic_expr1
-]
-
-tactic_expr1: [
+| ltac_expr4
+]
+
+ltac_expr4: [
+| ltac_expr3 ";" binder_tactic
+| ltac_expr3 ";" ltac_expr3
+| ltac_expr3 ";" tactic_then_locality tactic_then_gen "]"
+| ltac_expr3
+]
+
+ltac_expr3: [
+| "try" ltac_expr3
+| "do" int_or_var ltac_expr3
+| "timeout" int_or_var ltac_expr3
+| "time" OPT string ltac_expr3
+| "repeat" ltac_expr3
+| "progress" ltac_expr3
+| "once" ltac_expr3
+| "exactly_once" ltac_expr3
+| "infoH" ltac_expr3
+| "abstract" ltac_expr2
+| "abstract" ltac_expr2 "using" ident
+| selector ltac_expr3
+| ltac_expr2
+]
+
+ltac_expr2: [
+| ltac_expr1 "+" binder_tactic
+| ltac_expr1 "+" ltac_expr2
+| "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
+| ltac_expr1 "||" binder_tactic
+| ltac_expr1 "||" ltac_expr2
+| ltac_expr1
+]
+
+ltac_expr1: [
| match_key "goal" "with" match_context_list "end"
| match_key "reverse" "goal" "with" match_context_list "end"
-| match_key tactic_expr5 "with" match_list "end"
-| "first" "[" LIST0 tactic_expr5 SEP "|" "]"
-| "solve" "[" LIST0 tactic_expr5 SEP "|" "]"
+| match_key ltac_expr5 "with" match_list "end"
+| "first" "[" LIST0 ltac_expr5 SEP "|" "]"
+| "solve" "[" LIST0 ltac_expr5 SEP "|" "]"
| "idtac" LIST0 message_token
| failkw [ int_or_var | ] LIST0 message_token
| simple_tactic
| tactic_arg
| reference LIST0 tactic_arg_compat
-| tactic_expr0
+| ltac_expr0
]
-tactic_expr0: [
-| "(" tactic_expr5 ")"
+ltac_expr0: [
+| "(" ltac_expr5 ")"
| "[" ">" tactic_then_gen "]"
| tactic_atom
]
@@ -2005,8 +2005,8 @@ failkw: [
]
binder_tactic: [
-| "fun" LIST1 input_fun "=>" tactic_expr5
-| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
+| "fun" LIST1 input_fun "=>" ltac_expr5
+| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
]
tactic_arg_compat: [
@@ -2056,9 +2056,9 @@ input_fun: [
]
let_clause: [
-| identref ":=" tactic_expr5
-| "_" ":=" tactic_expr5
-| identref LIST1 input_fun ":=" tactic_expr5
+| identref ":=" ltac_expr5
+| "_" ":=" ltac_expr5
+| identref LIST1 input_fun ":=" ltac_expr5
]
match_pattern: [
@@ -2073,9 +2073,9 @@ match_hyps: [
]
match_context_rule: [
-| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
-| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
-| "_" "=>" tactic_expr5
+| LIST0 match_hyps SEP "," "|-" match_pattern "=>" ltac_expr5
+| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" ltac_expr5
+| "_" "=>" ltac_expr5
]
match_context_list: [
@@ -2084,8 +2084,8 @@ match_context_list: [
]
match_rule: [
-| match_pattern "=>" tactic_expr5
-| "_" "=>" tactic_expr5
+| match_pattern "=>" ltac_expr5
+| "_" "=>" ltac_expr5
]
match_list: [
@@ -2105,12 +2105,12 @@ ltac_def_kind: [
]
tacdef_body: [
-| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5
-| Constr.global ltac_def_kind tactic_expr5
+| Constr.global LIST1 input_fun ltac_def_kind ltac_expr5
+| Constr.global ltac_def_kind ltac_expr5
]
tactic: [
-| tactic_expr5
+| ltac_expr5
]
range_selector: [
@@ -2150,7 +2150,7 @@ G_LTAC_hint: [
]
G_LTAC_term0: [
-| "ltac" ":" "(" Pltac.tactic_expr ")"
+| "ltac" ":" "(" Pltac.ltac_expr ")"
]
ltac_selector: [
@@ -2502,7 +2502,7 @@ as_name: [
]
by_tactic: [
-| "by" tactic_expr3
+| "by" ltac_expr3
|
]
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 88e9ff13e8..5417a14e6d 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -11,7 +11,7 @@
(** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
(** The route of a generic argument, from parsing to evaluation.
-In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
+In the following diagram, "object" can be ltac_expr, constr, tactic_arg, etc.
{% \begin{verbatim} %}
parsing in_raw out_raw
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ad4374dba3..ff4a82f864 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
- Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
+ Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5)
(** Backward-compatible tactic notation entry names *)
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index f8fbf0c2d0..affcf814d7 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,21 +74,21 @@ let hint = G_proofs.hint
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
+ GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_arg command hint
tactic_mode constr_may_eval constr_eval toplevel_selector
term;
tactic_then_last:
- [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" ->
+ [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
{ Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) }
| -> { [||] }
] ]
;
tactic_then_gen:
- [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
- | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
+ [ [ ta = ltac_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
+ | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
| ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) }
- | ta = tactic_expr -> { ([ta], None) }
+ | ta = ltac_expr -> { ([ta], None) }
| "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
| -> { ([TacId []], None) }
] ]
@@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram
for [TacExtend] *)
[ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
;
- tactic_expr:
+ ltac_expr:
[ "5" RIGHTA
[ te = binder_tactic -> { te } ]
| "4" LEFTA
- [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
- | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
- | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+ [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
+ | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) }
+ | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
let (first,tail) = tg in
match l , tail with
| false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
@@ -111,40 +111,40 @@ GRAMMAR EXTEND Gram
| false , None -> TacThen (ta0,TacDispatch first)
| true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
- [ IDENT "try"; ta = tactic_expr -> { TacTry ta }
- | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
- | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) }
- | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) }
- | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta }
- | IDENT "progress"; ta = tactic_expr -> { TacProgress ta }
- | IDENT "once"; ta = tactic_expr -> { TacOnce ta }
- | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta }
- | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta }
+ [ 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 "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
+ | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
+ | IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
+ | IDENT "once"; ta = ltac_expr -> { TacOnce ta }
+ | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta }
+ | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta }
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
{ TacAbstract (tc,Some s) }
- | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ]
+ | sel = selector; ta = ltac_expr -> { TacSelect (sel, ta) } ]
(*End of To do*)
| "2" RIGHTA
- [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
- | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) }
- | IDENT "tryif" ; ta = tactic_expr ;
- "then" ; tat = tactic_expr ;
- "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) }
- | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
- | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ]
+ [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
+ | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) }
+ | IDENT "tryif" ; ta = ltac_expr ;
+ "then" ; tat = ltac_expr ;
+ "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) }
+ | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
+ | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ]
| "1" RIGHTA
[ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
{ TacMatchGoal (b,false,mrl) }
| b = match_key; IDENT "reverse"; IDENT "goal"; "with";
mrl = match_context_list; "end" ->
{ TacMatchGoal (b,true,mrl) }
- | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+ | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" ->
{ TacMatch (b,c,mrl) }
- | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacFirst l }
- | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacSolve l }
| IDENT "idtac"; l = LIST0 message_token -> { TacId l }
| g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
@@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram
| r = reference; la = LIST0 tactic_arg_compat ->
{ TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
| "0"
- [ "("; a = tactic_expr; ")" -> { a }
+ [ "("; a = ltac_expr; ")" -> { a }
| "["; ">"; tg = tactic_then_gen; "]" -> {
let (tf,tail) = tg in
begin match tail with
@@ -166,14 +166,14 @@ GRAMMAR EXTEND Gram
failkw:
[ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
;
- (* binder_tactic: level 5 of tactic_expr *)
+ (* binder_tactic: level 5 of ltac_expr *)
binder_tactic:
[ RIGHTA
- [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+ [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
{ TacFun (it,body) }
| "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
llc = LIST1 let_clause SEP "with"; "in";
- body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
+ body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
;
(* Tactic arguments to the right of an application *)
tactic_arg_compat:
@@ -223,11 +223,11 @@ GRAMMAR EXTEND Gram
| l = ident -> { Name.Name l } ] ]
;
let_clause:
- [ [ idr = identref; ":="; te = tactic_expr ->
+ [ [ idr = identref; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
- | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr ->
+ | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr ->
{ (na, arg_of_expr te) }
- | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+ | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ]
;
match_pattern:
@@ -251,18 +251,18 @@ GRAMMAR EXTEND Gram
;
match_context_rule:
[ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
+ "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
| "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_context_list:
[ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
| "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
;
match_rule:
- [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_list:
[ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
@@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram
(* Definitions for tactics *)
tacdef_body:
[ [ name = Constr.global; it=LIST1 input_fun;
- redef = ltac_def_kind; body = tactic_expr ->
+ redef = ltac_def_kind; body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
Tacexpr.TacticDefinition (id, TacFun (it, body)) }
| name = Constr.global; redef = ltac_def_kind;
- body = tactic_expr ->
+ body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
] ]
;
tactic:
- [ [ tac = tactic_expr -> { tac } ] ]
+ [ [ tac = ltac_expr -> { tac } ] ]
;
range_selector:
@@ -344,7 +344,7 @@ GRAMMAR EXTEND Gram
{ Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
term: LEVEL "0"
- [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+ [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->
{ let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ]
;
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 18fc9ce9d4..7b020c40ba 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram
[ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
;
by_tactic:
- [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+ [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac }
| -> { None } ] ]
;
rewriter :
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index b7b54143df..1631215d58 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -38,7 +38,8 @@ let clause_dft_concl =
(* Main entries for ltac *)
let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+let ltac_expr = Entry.create "ltac_expr"
+let tactic_expr = ltac_expr
let binder_tactic = Entry.create "binder_tactic"
let tactic = Entry.create "tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 8565c4b4d6..a2424d4c60 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -32,7 +32,9 @@ val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
val in_clause : Names.lident Locus.clause_expr Entry.t
val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
val tactic_arg : raw_tactic_arg Entry.t
+val ltac_expr : raw_tactic_expr Entry.t
val tactic_expr : raw_tactic_expr Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
val binder_tactic : raw_tactic_expr Entry.t
val tactic : raw_tactic_expr Entry.t
val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6a9fb5c2ea..5e199dad62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** This module implements pretty-printers for tactic_expr syntactic
+(** This module implements pretty-printers for ltac_expr syntactic
objects and their subcomponents. *)
open Genarg
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 6823b6411f..159ca678e9 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -33,7 +33,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol
let atactic n =
if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
- else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+ else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
@@ -116,7 +116,7 @@ let get_tactic_entry n =
else if Int.equal n 5 then
Pltac.binder_tactic, None
else if 1<=n && n<5 then
- Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
+ Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n))
else
user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
@@ -383,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
in
List.iteri iter (List.rev prods);
(* We call [extend_atomic_tactic] only for "basic tactics" (the ones
- at tactic_expr level 0) *)
+ at ltac_expr level 0) *)
if Int.equal level 0 then extend_atomic_tactic name prods
(**********************************************************************)
@@ -555,7 +555,7 @@ let print_located_tactic qid =
let () =
let entries = [
- AnyEntry Pltac.tactic_expr;
+ AnyEntry Pltac.ltac_expr;
AnyEntry Pltac.binder_tactic;
AnyEntry Pltac.simple_tactic;
AnyEntry Pltac.tactic_arg;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 22b9abda20..7728415ddd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1997,7 +1997,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
(* MUST be marshallable! *)
-type tactic_expr = {
+type ltac_expr = {
global: bool;
ast: Tacexpr.raw_tactic_expr;
}
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index dba9c938ec..fe3079198c 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,12 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
-type tactic_expr = {
+type ltac_expr = {
global: bool;
ast: Tacexpr.raw_tactic_expr;
}
-val hide_interp : tactic_expr -> ComTactic.interpretable
+val hide_interp : ltac_expr -> ComTactic.interpretable
(** Internals that can be useful for syntax extensions. *)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 77360052f8..70dab585bf 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtacarg;
- ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
+ ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
END
(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
@@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: ssrtac3arg;
- ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+ ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
END
{
@@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram
| n = Prim.natural -> { ArgArg (check_index ~loc n) }
] ];
ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
- ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]];
+ ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
ssrseqarg: [
[ arg = ssrswap -> { noindex, swaptacarg arg }
| i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
| i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
- | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
+ | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
] ];
END
{
-let tactic_expr = Pltac.tactic_expr
+let ltac_expr = Pltac.ltac_expr
}
@@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "1" [ RIGHTA
- [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "1" [ RIGHTA
+ [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
] ];
END
@@ -1704,9 +1704,9 @@ END
(* (Removing user-specified parentheses is dubious anyway). *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
- tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
+ GLOBAL: ltac_expr;
+ ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
+ ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
(** The internal "done" and "ssrautoprop" tactics. *)
@@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1)
(* The latter two are used in forward-chaining tactics (have, suffice, wlog) *)
(* and subgoal reordering tacticals (; first & ; last), respectively. *)
-(* Force use of the tactic_expr parsing entry, to rule out tick marks. *)
+(* Force use of the ltac_expr parsing entry, to rule out tick marks. *)
(** The "by" tactical. *)
@@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssrdotac: [
- [ tac = tactic_expr LEVEL "3" -> { mk_hint tac }
+ [ tac = ltac_expr LEVEL "3" -> { mk_hint tac }
| tacs = ssrortacarg -> { tacs }
] ];
- tactic_expr: LEVEL "3" [ RIGHTA
+ ltac_expr: LEVEL "3" [ RIGHTA
[ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses ->
{ ssrdotac_expr ~loc noindex m tac clauses }
| IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
@@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg =
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
+ GLOBAL: ltac_expr;
ssr_first: [
[ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats }
- | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl }
+ | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl }
] ];
ssr_first_else: [
[ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) }
| tac = ssr_first -> { tac } ]];
- tactic_expr: LEVEL "4" [ LEFTA
- [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
+ ltac_expr: LEVEL "4" [ LEFTA
+ [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
{ TacThen (tac1, tac2) }
- | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac L2R arg }
- | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg ->
+ | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg ->
{ tclseq_expr ~loc tac R2L arg }
] ];
END
@@ -2447,8 +2447,8 @@ END
(* The standard TACTIC EXTEND does not work for abstract *)
GRAMMAR EXTEND Gram
- GLOBAL: tactic_expr;
- tactic_expr: LEVEL "3"
+ GLOBAL: ltac_expr;
+ ltac_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
{ ssrtac_expr ~loc "abstract"
[Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 2da5344496..cc2cdf7ef8 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -80,7 +80,7 @@ let tac2def_syn = Entry.create "tac2def_syn"
let tac2def_mut = Entry.create "tac2def_mut"
let tac2mode = Entry.create "ltac2_command"
-let ltac1_expr = Pltac.tactic_expr
+let ltac1_expr = Pltac.ltac_expr
let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:09:56 +0000