From aba594ca194390bb00f8ef60ef8a5eef6694fc07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 10 Mar 2021 12:17:32 +0100
Subject: Regenerate the Ltac2 syntax for documentation.

---
 doc/tools/docgram/common.edit_mlg | 1 +
 1 file changed, 1 insertion(+)

(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 24ecc65e9b..fd1c3c0260 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2730,6 +2730,7 @@ SPLICE: [
 | variance_identref
 | rewriter
 | conversion
+| type_cast
 ] (* end SPLICE *)
 
 RENAME: [
-- 
cgit v1.2.3