aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/ltac.rst2
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst2
-rw-r--r--doc/tools/docgram/common.edit_mlg16
-rw-r--r--doc/tools/docgram/fullGrammar16
-rw-r--r--doc/tools/docgram/orderedGrammar10
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg12
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
8 files changed, 31 insertions, 31 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2a102adfcc..f18569c7fd 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -876,7 +876,7 @@ Print/identity tactic: idtac
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. tacn:: idtac {* {| @ident | @string | @integer } }
+.. tacn:: idtac {* {| @ident | @string | @natural } }
:name: idtac
Leaves the proof unchanged and prints the given tokens. Strings and integers are printed
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b4f32c6cbb..773e393eb6 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1159,7 +1159,7 @@ Match on values
Notations
---------
-.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr
+.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr
:name: Ltac2 Notation
.. todo seems like name maybe should use lident rather than ident, considering:
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ea60fa22d6..66b6ffac89 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1201,11 +1201,11 @@ command: [
| REPLACE "Next" "Obligation" "of" ident withtac
| WITH "Next" "Obligation" OPT ( "of" ident ) withtac
| DELETE "Next" "Obligation" withtac
-| REPLACE "Obligation" integer "of" ident ":" lglob withtac
-| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac )
-| DELETE "Obligation" integer "of" ident withtac
-| DELETE "Obligation" integer ":" lglob withtac
-| DELETE "Obligation" integer withtac
+| REPLACE "Obligation" natural "of" ident ":" lglob withtac
+| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| DELETE "Obligation" natural "of" ident withtac
+| DELETE "Obligation" natural ":" lglob withtac
+| DELETE "Obligation" natural withtac
| REPLACE "Obligations" "of" ident
| WITH "Obligations" OPT ( "of" ident )
| DELETE "Obligations"
@@ -1232,10 +1232,10 @@ command: [
| REPLACE "Solve" "All" "Obligations" "with" tactic
| WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
| DELETE "Solve" "All" "Obligations"
-| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic
-| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic
+| REPLACE "Solve" "Obligation" natural "of" ident "with" tactic
+| WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic
| DELETE "Solve" "Obligations"
-| DELETE "Solve" "Obligation" integer "with" tactic
+| DELETE "Solve" "Obligation" natural "with" tactic
| REPLACE "Solve" "Obligations" "of" ident "with" tactic
| WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
| DELETE "Solve" "Obligations" "with" tactic
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 994447b12d..9614fc06fe 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -606,14 +606,14 @@ command: [
| "Locate" "Ltac" reference
| "Ltac" LIST1 ltac_tacdef_body SEP "with"
| "Print" "Ltac" "Signatures"
-| "Obligation" integer "of" ident ":" lglob withtac
-| "Obligation" integer "of" ident withtac
-| "Obligation" integer ":" lglob withtac
-| "Obligation" integer withtac
+| "Obligation" natural "of" ident ":" lglob withtac
+| "Obligation" natural "of" ident withtac
+| "Obligation" natural ":" lglob withtac
+| "Obligation" natural withtac
| "Next" "Obligation" "of" ident withtac
| "Next" "Obligation" withtac
-| "Solve" "Obligation" integer "of" ident "with" tactic
-| "Solve" "Obligation" integer "with" tactic
+| "Solve" "Obligation" natural "of" ident "with" tactic
+| "Solve" "Obligation" natural "with" tactic
| "Solve" "Obligations" "of" ident "with" tactic
| "Solve" "Obligations" "with" tactic
| "Solve" "Obligations"
@@ -2099,7 +2099,7 @@ match_list: [
message_token: [
| identref
| STRING
-| integer
+| natural
]
ltac_def_kind: [
@@ -2811,7 +2811,7 @@ sexpr: [
syn_level: [
| (* Ltac2 plugin *)
-| ":" Prim.integer (* Ltac2 plugin *)
+| ":" Prim.natural (* Ltac2 plugin *)
]
tac2def_syn: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 8d4e0189e6..bbc4edf199 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -835,9 +835,9 @@ command: [
| "Comments" LIST0 [ one_term | string | natural ]
| "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
| "Declare" "Scope" scope_name
-| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
+| "Obligation" natural OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
| "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
-| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr
+| "Solve" "Obligation" natural OPT ( "of" ident ) "with" ltac_expr
| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
| "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
| "Admit" "Obligations" OPT ( "of" ident )
@@ -996,7 +996,7 @@ command: [
| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
| "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
-| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" natural ) ":=" ltac2_expr
| "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr (* Ltac2 plugin *)
| "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *)
@@ -1425,8 +1425,8 @@ simple_tactic: [
| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
| "first" "[" LIST0 ltac_expr SEP "|" "]"
| "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 [ ident | string | integer ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ]
+| "idtac" LIST0 [ ident | string | natural ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ]
| "fun" LIST1 name "=>" ltac_expr
| "eval" red_expr "in" term
| "context" ident "[" term "]"
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 114acaa412..78cde2cde8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram
message_token:
[ [ id = identref -> { MsgIdent id }
| s = STRING -> { MsgString s }
- | n = integer -> { MsgInt n } ] ]
+ | n = natural -> { MsgInt n } ] ]
;
ltac_def_kind:
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fa176482bf..a6673699af 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" natural(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
@@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index bec9632e84..d42a935104 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -371,7 +371,7 @@ GRAMMAR EXTEND Gram
;
syn_level:
[ [ -> { None }
- | ":"; n = Prim.integer -> { Some n }
+ | ":"; n = Prim.natural -> { Some n }
] ]
;
tac2def_syn:
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:33:50 +0000