Experimenting using a record for decl_notation.

4 files changed, 28 insertions, 5 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f2a533fdb2..c1414c552a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -379,7 +379,9 @@ GRAMMAR EXTEND Gram
   ;
   decl_notation:
     [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing;
-        scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,b,scopt) } ] ]
+        scopt = OPT [ ":"; sc = IDENT -> { sc } ] ->
+      { { decl_ntn_string = ntn; decl_ntn_interp = c;
+          decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ]
   ;
   decl_sep:
     [ [ IDENT "and" -> { () } ] ]
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 7a150e021b..33fd14a731 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1654,11 +1654,21 @@ let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
 
 (* Notations with only interpretation *)
 
-let add_notation_interpretation env ({CAst.loc;v=df},c,onlyparse,sc) =
+let add_notation_interpretation env decl_ntn =
+  let
+    { decl_ntn_string = { CAst.loc ; v = df };
+      decl_ntn_interp = c;
+      decl_ntn_only_parsing = onlyparse;
+      decl_ntn_scope = sc } = decl_ntn in
   let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in
   Dumpglob.dump_notation (loc,df') sc true
 
-let set_notation_for_interpretation env impls ({CAst.v=df},c,onlyparse,sc) =
+let set_notation_for_interpretation env impls decl_ntn =
+  let
+    { decl_ntn_string = { CAst.v = df };
+      decl_ntn_interp = c;
+      decl_ntn_only_parsing = onlyparse;
+      decl_ntn_scope = sc } = decl_ntn in
   (try ignore
     (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ());
   with NoSyntaxRule ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 48961fd271..84ae04e4cc 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -416,7 +416,13 @@ let string_of_theorem_kind = let open Decls in function
   let pr_only_parsing_clause onlyparsing =
     pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
 
-  let pr_decl_notation prc ({loc; v=ntn},c,onlyparsing, scopt) =
+  let pr_decl_notation prc decl_ntn =
+    let open Vernacexpr in
+    let
+      { decl_ntn_string = {CAst.loc;v=ntn};
+        decl_ntn_interp = c;
+        decl_ntn_only_parsing = onlyparsing;
+        decl_ntn_scope = scopt } = decl_ntn in
     fnl () ++ keyword "where " ++ qs ntn ++ str " := "
     ++ Flags.without_option Flags.beautify prc c
     ++ pr_only_parsing_clause onlyparsing
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b6514487e8..7169ea834a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -128,7 +128,12 @@ type definition_expr =
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
-type decl_notation = lstring * constr_expr * bool * scope_name option
+type decl_notation =
+  { decl_ntn_string : lstring
+  ; decl_ntn_interp : constr_expr
+  ; decl_ntn_only_parsing : bool
+  ; decl_ntn_scope : scope_name option
+  }
 
 type 'a fix_expr_gen =
   { fname : lident