diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index c770df051..8115376c9 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1276,13 +1276,13 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> + ( Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> Tacmach.New.pf_last_hyp >>- fun hyp -> let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)) in - Goal.concl >>- fun concl -> + Proofview.Goal.concl >>- fun concl -> Tacticals.New.tclFIRST ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac:: (List.map Tacticals.New.tclCOMPLETE @@ -1434,7 +1434,7 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d)) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Goal.concl >>- fun concl -> + ( Proofview.Goal.concl >>- fun concl -> let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map |