From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:12:00 +0200
Subject: [numeral notation] Adding the via ... using ... option

This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
---
 doc/tools/docgram/common.edit_mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 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 5d0f9208fc..4d615a130a 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1285,10 +1285,10 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier
-| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier
-| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier
-| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier
+| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
+| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
+| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
+| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
-- 
cgit v1.2.3