diff options
| author | Pierre-Marie Pédrot | 2020-05-09 15:56:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 5e1da5b05860750606f32063a221d6023cabf5dc (patch) | |
| tree | fdc2927a9ad56a7745b22e33610af8aee3442518 /plugins | |
| parent | 2e53445be16ef28058599fed3f06424db17f6943 (diff) | |
Tweak the error message of reference internalization.
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} -> |