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 /plugins/ltac | |
| 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 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 12 |
2 files changed, 7 insertions, 7 deletions
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 |