diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f4408d403..b443a357a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2975,7 +2975,7 @@ let specialize (c,lbind) ipat = if occur_meta clause.evd term then user_err (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ + Name.print (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in |