aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/setoid_replace.ml')
-rw-r--r--tactics/setoid_replace.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 269c40fec3..23e732797a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -108,7 +108,9 @@ let current_constant id =
try
global_reference id
with Not_found ->
- anomaly ("Setoid: cannot find " ^ (string_of_id id))
+ anomalylabstrm ""
+ (str "Setoid: cannot find " ++ pr_id id ++
+ str "(if loading Setoid.v under coqtop, use option \"-top Coq.Setoids.Setoid\")")
(* From Setoid.v *)