diff options
| -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 |