diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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} -> |