diff options
| author | Jason Gross | 2018-08-14 20:19:07 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | 581bbbb23fcb488d5c1a10f360a6705a6792b2b1 (patch) | |
| tree | e0250040e842e1aaa68699a8ce1703195baeff22 /plugins | |
| parent | 6a280b70fc66ff0231a9945cc3b3718385d3971c (diff) | |
Add periods in response to PR comments
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/numeral.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 901d4f0cb4..8dced1a8de 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -242,8 +242,9 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) | _ -> let (sigma, env) = Pfedit.get_current_context () in CErrors.user_err ?loc - (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma c) + (strbrk "Unexpected term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") let no_such_number ?loc ty = CErrors.user_err ?loc @@ -256,8 +257,9 @@ let interp_option ty ?loc c = | App (_None, [| _ |]) -> no_such_number ?loc ty | x -> let (sigma, env) = Pfedit.get_current_context () in CErrors.user_err ?loc - (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma c) + (strbrk "Unexpected non-option term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") let uninterp_option c = match Constr.kind c with @@ -440,7 +442,7 @@ let vernac_numeral_notation ty f g scope opts = get_constructors ind | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err - (pr_qualid ty ++ str " is not an inductive type") + (pr_qualid ty ++ str " is not an inductive type.") in (* Check the type of f *) let to_kind = |