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/orderedGrammar | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index bbc4edf199..aae96fc966 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -896,6 +896,7 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
+| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
@@ -1614,7 +1615,7 @@ simple_tactic: [
 | "change_no_check" conversion OPT clause_dft_concl
 | "btauto"
 | "rtauto"
-| "congruence" OPT integer OPT ( "with" LIST1 one_term )
+| "congruence" OPT natural OPT ( "with" LIST1 one_term )
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
-- 
cgit v1.2.3