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