From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 doc/tools/docgram/common.edit_mlg | 7 ++++---
 1 file changed, 4 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 e43583de09..5de1f09c53 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1289,8 +1289,8 @@ command: [
 | WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name
 | REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
 | WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier
-| REPLACE "String" "Notation" reference reference reference ":" ident
-| WITH "String" "Notation" reference reference reference ":" scope_name
+| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident
+| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name
 
 | DELETE "Ltac2" ltac2_entry      (* was split up *)
 | DELETE "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
@@ -2460,8 +2460,9 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
-| number_mapping
+| number_string_mapping
 | number_options
+| string_option
 ] (* end SPLICE *)
 
 RENAME: [
-- 
cgit v1.2.3