diff options
| author | Pierre-Marie Pédrot | 2020-07-18 11:45:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-18 11:47:13 +0200 |
| commit | bece6859bf6ee3e652c2e6e5596312580edc7e1d (patch) | |
| tree | b6250d350a365d3f237dce4f107f2e03b4608cef | |
| parent | 4b4daabe115a0386295f1c2bc025c5ce3bdf0065 (diff) | |
Clarify the Ltac2 invalid identifier message.
| -rw-r--r-- | user-contrib/Ltac2/tac2quote.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index 3aea2bea8d..b346b3ee5c 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -88,7 +88,8 @@ let inj_wit ?loc wit x = let of_variable {loc;v=id} = let qid = Libnames.qualid_of_ident ?loc id in if Tac2env.is_constructor qid then - CErrors.user_err ?loc (str "Invalid identifier") + CErrors.user_err ?loc (str "Invalid identifier" ++ spc () ++ Id.print id ++ + spc () ++ str "classifying as an Ltac2 constructor") else CAst.make ?loc @@ CTacRef (RelId qid) let of_anti f = function |