diff options
| author | Pierre Roux | 2020-09-08 10:41:03 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 (patch) | |
| tree | 89834f9ed7d88379f9284d93947b6f7d54cef1ff /doc/tools/docgram/orderedGrammar | |
| parent | 031cc2ba1a19a06766df85b8693c72f16fa62de6 (diff) | |
Turn integer into natural in several mlgs
Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 10 |
1 files changed, 5 insertions, 5 deletions
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 "]" |