diff options
| -rw-r--r-- | vernac/g_vernac.mlg | 4 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 14 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 7 |
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 |