From 5e1da5b05860750606f32063a221d6023cabf5dc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 May 2020 15:56:55 +0200
Subject: Tweak the error message of reference internalization.

---
 plugins/ltac/tacintern.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fcedbe8e2e..53dc518bd3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -302,8 +302,14 @@ let evalref_of_globref ?loc ?short = function
   | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
   | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
   | r ->
-    user_err ?loc (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
-     spc () ++ str "to an evaluable reference.")
+    let tpe = match r with
+    | GlobRef.IndRef _ -> "inductive"
+    | GlobRef.ConstructRef _ -> "constructor"
+    | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+    in
+    user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+      Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+      str "into an evaluable reference.")
 
 let intern_evaluable ist = function
   | {v=AN qid} ->
-- 
cgit v1.2.3