Ali Caglayan (Aug 12 2021 at 18:57): 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?
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: Dec 05 2023 at 11:01 UTC