aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4fb4b3263..a170c27fb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -327,7 +327,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
- let hyp = Context.map_named_declaration nf decl in
+ let hyp = Context.Named.Declaration.map nf decl in
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list
(Hint_db.add_list env sigma hintl local_db)