From 2a5e88b967f648887219e80aaf694395f1f15c1c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 12 Jan 2021 22:01:40 +0100
Subject: Adjust the doc_grammar files.

---
 doc/tools/docgram/orderedGrammar | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index d950b32160..2a47124667 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -2381,7 +2381,7 @@ ltac2_quotations: [
 | "ident" ":" "(" lident ")"
 | "constr" ":" "(" term ")"
 | "open_constr" ":" "(" term ")"
-| "pattern" ":" "(" cpattern ")"
+| "pat" ":" "(" cpattern ")"
 | "reference" ":" "(" [ "&" ident | qualid ] ")"
 | "ltac1" ":" "(" ltac1_expr_in_env ")"
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"
-- 
cgit v1.2.3