aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:50:36 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:50:36 +0100
commitb3a8761790c0905aad8e5d3102fab606fe5e7fd6 (patch)
treece5fbe8cb717bad677ad755e7875413d3e5d0e84 /vernac/classes.ml
parent9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (diff)
parent886a9c2fb25e32bd87b3fce38023b3e701134d23 (diff)
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
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]