diff options
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index bce208df6e..f9f65a8c30 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1664,7 +1664,7 @@ let add_notation_interpretation env decl_ntn = decl_ntn_scope = sc; } = decl_ntn in match interp_non_syntax_modifiers modifiers with - | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here") + | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.") | Some (only_parsing,only_printing,entry) -> let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in Dumpglob.dump_notation (loc,df') sc true |