diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 11 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 28 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 2 |
3 files changed, 24 insertions, 17 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 74cb7a364f..42230dff17 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 diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d70275dee5..54e4405d1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -221,18 +221,22 @@ let auto_unif_flags freeze st = resolve_evars = false } -let e_give_exact flags poly (c,clenv) gl = +let e_give_exact flags poly (c,clenv) = + let open Tacmach.New in + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = project gl in let (c, _, _) = c in - let c, gl = + let c, sigma = if poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in + let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in let c = Vars.subst_univs_level_constr subst c in - c, {gl with sigma = evd} - else c, gl + c, evd + else c, sigma in - let t1 = pf_unsafe_type_of gl c in - Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl + let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in + Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma) + end } let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in @@ -455,7 +459,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else - Proofview.V82.tactic (e_give_exact flags poly (c,clenv)) + e_give_exact flags poly (c,clenv) | Res_pf_THEN_trivial_fail (term,cl) -> let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in let snd = if complete then Tacticals.New.tclIDTAC @@ -1613,9 +1617,11 @@ let not_evar c = | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") | _ -> Proofview.tclUNIT () -let is_ground c gl = - if Evarutil.is_ground_term (project gl) c then tclIDTAC gl - else tclFAIL 0 (str"Not ground") gl +let is_ground c = + let open Tacticals.New in + Proofview.tclEVARMAP >>= fun sigma -> + if Evarutil.is_ground_term sigma c then tclIDTAC + else tclFAIL 0 (str"Not ground") let autoapply c i = let open Proofview.Notations in diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index a38be5972f..738cc0feba 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic val not_evar : constr -> unit Proofview.tactic -val is_ground : constr -> tactic +val is_ground : constr -> unit Proofview.tactic val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic |