diff options
| author | Hugo Herbelin | 2020-09-09 20:24:46 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | d5eb564a1ae46409e90a2c6bd6af5b77aa37773e (patch) | |
| tree | 01d09a9564b95d5af908590923ae2c2202b144f3 /doc/tools/docgram/common.edit_mlg | |
| parent | 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 (diff) | |
Adding a wit_natural standard argument.
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 66b6ffac89..a22f7ae9f3 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1087,10 +1087,10 @@ simple_tactic: [ | WITH "subst" OPT ( LIST1 var ) | DELETE "subst" | DELETE "congruence" -| DELETE "congruence" integer +| DELETE "congruence" natural | DELETE "congruence" "with" LIST1 constr -| REPLACE "congruence" integer "with" LIST1 constr -| WITH "congruence" OPT integer OPT ( "with" LIST1 constr ) +| REPLACE "congruence" natural "with" LIST1 constr +| WITH "congruence" OPT natural OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] |