Stream: Coq devs & plugin devs

Topic: How to suggest command in error message


view this post on Zulip Ali Caglayan (Aug 12 2021 at 18:57):

I'm writing a user error message, but I want to suggest a vernac command for the user to try in order to fix it. Are there any errors which suggest vernac commands that I can take precedence from?

view this post on Zulip Jason Gross (Aug 18 2021 at 17:44):

    user_err Pp.(prlist str
        ["The following section "; (String.plural n "variable"); " ";
        (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
        missing_vars ++ str "." ++ fnl () ++ fnl () ++
        str "You can either update your proof to not depend on " ++ missing_vars ++
        str ", or you can update your Proof line from" ++ fnl () ++
        str "Proof using " ++ declared_vars ++ fnl () ++
        str "to" ++ fnl () ++
        str "Proof using " ++ inferred_vars)

in kernel/term_typing.ml suggests the vernacular Proof using


Last updated: Oct 16 2021 at 02:03 UTC