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/common.edit_mlg | |
| 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/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 16 |
1 files changed, 8 insertions, 8 deletions
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 |