diff options
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 ] |