diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-16 20:37:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:59:21 +0200 |
| commit | 98da9fdce866728f93bc7cb690275f5559aa9bae (patch) | |
| tree | bc01065a1cca18ded5aa221e3c9e1a7c7ad316d8 /tactics/auto.ml | |
| parent | a1fd5fb489237a1300adb242e2c9b6c74c82981b (diff) | |
Removing various tactic compatibility layers in core tactics.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 74cb7a364..42230dff1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) - | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") + | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") } | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN @@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= with "debug auto" we don't display the details of inner trivial *) (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db) | Unfold_nth c -> - Proofview.V82.tactic (fun gl -> - if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl - else tclFAIL 0 (str"Unbound reference") gl) + Proofview.Goal.enter { enter = begin fun gl -> + if exists_evaluable_reference (Tacmach.New.pf_env gl) c then + Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) + else Tacticals.New.tclFAIL 0 (str"Unbound reference") + end } | Extern tacast -> conclPattern concl p tacast in |