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/fullGrammar | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/tools/docgram/fullGrammar') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c764cb6f37..914347b4cf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numeral_modifier -| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier +| "Number" "Notation" reference reference reference ":" ident number_modifier +| "Numeral" "Notation" reference reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,7 +2549,7 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" -- 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/fullGrammar | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'doc/tools/docgram/fullGrammar') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 914347b4cf..8a0feb0e2f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident number_modifier -| "Numeral" "Notation" reference reference reference ":" ident number_modifier +| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2555,6 +2555,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| reference reference +] + +number_via: [ +| "via" reference "using" "(" LIST1 number_using SEP "," ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) -- 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/fullGrammar | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'doc/tools/docgram/fullGrammar') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 8a0feb0e2f..17fc220f6c 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Number" "Notation" reference reference reference OPT number_options ":" ident +| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,18 +2549,28 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| reference reference +number_mapping: [ +| reference "=>" reference ] number_via: [ -| "via" reference "using" "(" LIST1 number_using SEP "," ")" +| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +] + +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via +] + +number_options: [ +| "(" LIST1 number_modifier SEP "," ")" ] tac2pat1: [ -- cgit v1.2.3 From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:23:00 +0200 Subject: [numeral notation] Handle implicit arguments --- doc/tools/docgram/fullGrammar | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/tools/docgram/fullGrammar') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 17fc220f6c..3a0c3a8bc7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2557,6 +2557,7 @@ deprecated_number_modifier: [ number_mapping: [ | reference "=>" reference +| "[" reference "]" "=>" reference ] number_via: [ -- 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/fullGrammar | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'doc/tools/docgram/fullGrammar') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3a0c3a8bc7..826a0b6f36 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -688,7 +688,7 @@ command: [ | "Print" "Fields" (* ring plugin *) | "Number" "Notation" reference reference reference OPT number_options ":" ident | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier -| "String" "Notation" reference reference reference ":" ident +| "String" "Notation" reference reference reference OPT string_option ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) @@ -2555,25 +2555,29 @@ deprecated_number_modifier: [ | "(" "abstract" "after" bignat ")" ] -number_mapping: [ +number_string_mapping: [ | reference "=>" reference | "[" reference "]" "=>" reference ] -number_via: [ -| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +number_string_via: [ +| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]" ] number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] number_options: [ | "(" LIST1 number_modifier SEP "," ")" ] +string_option: [ +| "(" number_string_via ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) -- cgit v1.2.3