From d5eb564a1ae46409e90a2c6bd6af5b77aa37773e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2020 20:24:46 +0200
Subject: Adding a wit_natural standard argument.

---
 doc/tools/docgram/common.edit_mlg | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

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 ]
-- 
cgit v1.2.3