diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 0dd90246d..ec3a8d6c9 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -581,7 +581,7 @@ let add_hints local dbnames0 h = add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> - let pat = Option.map (Constrintern.interp_constrpattern Evd.empty (Global.env())) patcom in + let pat = Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in add_externs pri pat tacexp local dbnames | HintsDestruct(na,pri,loc,pat,code) -> |