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 0533d0d43..cd5eff4e7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -52,7 +52,7 @@ let _ =
let open Vernacexpr in
{ info with hint_pattern =
Option.map
- (Constrintern.intern_constr_pattern (Global.env()))
+ (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
info.hint_pattern } in
Flags.silently (fun () ->
Hints.add_hints local [typeclasses_db]