aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6d4b164b..ab1892a18 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -68,7 +68,7 @@ let _ =
let existing_instance glob g info =
let c = global g in
let info = Option.default Hints.empty_hint_info info in
- let instance = Global.type_of_global_unsafe c in
+ let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
let _, r = decompose_prod_assum instance in
match class_of_constr Evd.empty (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob