diff options
| author | Hugo Herbelin | 2020-10-31 22:15:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-06 17:40:53 +0200 |
| commit | bf6a5e1c7b10d6ff5686cc4a3e71eb105d7a0473 (patch) | |
| tree | d5cb9b84eeb5c81097abf67eb06e0d1a8c403011 | |
| parent | 9374aeeda2a3bc64774753862eae39a8e8539bb7 (diff) | |
Missing dot in an error message.
| -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 |