diff options
| author | Jim Fehrle | 2020-11-18 13:18:04 -0800 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-20 11:29:46 +0100 |
| commit | e74d328b32634a44ab049f971ec33fe6cd24df72 (patch) | |
| tree | 394780675ccac50c7e4848e7fba465002a17c5f3 /plugins/micromega | |
| parent | a8a0285c153cab810dedba6bae5a2a6a6d2c4333 (diff) | |
Use nat_or_var where negative values don't make sense
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/g_micromega.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index 40eea91b31..852a485329 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -29,7 +29,7 @@ open Tacarg DECLARE PLUGIN "micromega_plugin" TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i +| [ "psatz_Z" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) } | [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) } @@ -74,12 +74,12 @@ TACTIC EXTEND LRA_R END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_R" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) } | [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_Q" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) } | [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } END |