aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a95e6b941..fe163cabc 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -581,7 +581,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
(fun (path,info,c) ->
let info =
{ info with Vernacexpr.hint_pattern =
- Option.map (Constrintern.intern_constr_pattern env)
+ Option.map (Constrintern.intern_constr_pattern env sigma)
info.Vernacexpr.hint_pattern }
in
make_resolves env sigma ~name:(PathHints path)