diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 | ||||
| -rw-r--r-- | plugins/syntax/numeral.ml | 12 |
2 files changed, 10 insertions, 8 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2f7a7d42c1..6f655340da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1443,19 +1443,19 @@ Numeral notations The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @type is not an inductive type + .. exn:: @type is not an inductive type. Numeral notations can only be declared for inductive types with no arguments. - .. exn:: Unexpected term while parsing a numeral notation + .. exn:: Unexpected term @term while parsing a numeral notation. Parsing functions must always return ground terms, made up of applications of constructors and inductive types. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term while parsing a numeral notation + .. exn:: Unexpected non-option term @term while parsing a numeral notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a 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 = |