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/fullGrammar | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc/tools/docgram/fullGrammar')

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 9614fc06fe..2ee8e4347e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -689,6 +689,7 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
+| "Number" "Notation" reference reference reference ":" ident numnotoption
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
@@ -1435,9 +1436,9 @@ constr_as_binder_kind: [
 simple_tactic: [
 | "btauto"
 | "congruence"
-| "congruence" integer
+| "congruence" natural
 | "congruence" "with" LIST1 constr
-| "congruence" integer "with" LIST1 constr
+| "congruence" natural "with" LIST1 constr
 | "f_equal"
 | "firstorder" OPT tactic firstorder_using
 | "firstorder" OPT tactic "with" LIST1 preident
-- 
cgit v1.2.3