From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:13:44 +0200 Subject: Renaming numnotoption into number_modifier --- doc/tools/docgram/common.edit_mlg | 10 +++++----- 1 file changed, 5 insertions(+), 5 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 f6a684bbd7..5d0f9208fc 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 numeral_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier +| 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 "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,7 +1358,7 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -numeral_modifier: [ +number_modifier: [ | OPTINREF ] -- cgit v1.2.3 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 From c217bbe80e18255ee3e67fa6266736529d80636d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:14:00 +0200 Subject: [numeral notation] Document the via ... using ... option --- doc/tools/docgram/common.edit_mlg | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 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 4d615a130a..e43583de09 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 "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 "Number" "Notation" reference reference reference OPT number_options ":" ident +| 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 @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -number_modifier: [ -| OPTINREF -] - binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 @@ -2464,6 +2460,8 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_mapping +| number_options ] (* end SPLICE *) RENAME: [ -- cgit v1.2.3 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