diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/elim.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
6 files changed, 12 insertions, 15 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 485559898..cfbcc4750 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -164,7 +164,7 @@ let e_give_exact flags poly (c,clenv) gl = else c, gl in let t1 = pf_unsafe_type_of gl c in - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl + Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6bbd9b2e8..f0f408c24 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -33,7 +33,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c = let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then - Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) + Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) else exact_check c end } diff --git a/tactics/elim.ml b/tactics/elim.ml index 33eb80c28..d59c2fba4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -84,7 +84,7 @@ let general_decompose recognizer c = (onLastHypId (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); - Proofview.V82.tactic (exact_no_check c) ] + exact_no_check c ] end } let head_in indl t gl = diff --git a/tactics/equality.ml b/tactics/equality.ml index eecc2b787..572d4b7ab 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1582,7 +1582,7 @@ let substClause l2r c cls = Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) - [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] + [Proofview.tclUNIT (); exact_no_check c] end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01af30049..6bf5831f7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1833,7 +1833,7 @@ let cut_and_apply c = (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) -let new_exact_no_check c = +let exact_no_check c = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } let exact_check c = @@ -1845,13 +1845,11 @@ let exact_check c = let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in let tac = - Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) in Sigma.Unsafe.of_pair (tac, sigma) end } -let exact_no_check = Tacmach.refine_no_check - let vm_cast_no_check c gl = let concl = Tacmach.pf_concl gl in Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl @@ -2626,8 +2624,7 @@ let forward b usetac ipat c = Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in let hd = head_ident c in - Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) - (Proofview.V82.tactic (exact_no_check c)) + Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) end } | Some tac -> if b then @@ -2820,14 +2817,14 @@ let specialize (c,lbind) = (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHENFIRST (assert_before_replacing id typ) - (new_exact_no_check term)) + (exact_no_check term)) | _ -> (* To deprecate in favor of generalize? *) Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHENLAST (cut typ) - (new_exact_no_check term)) + (exact_no_check term)) end } (*****************************) @@ -3652,7 +3649,7 @@ let specialize_eqs id gl = let ty' = Evarutil.nf_evar !evars ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') - (exact_no_check ((* refresh_universes_strict *) acc')) gl + (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl @@ -4798,7 +4795,7 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> - new_exact_no_check (applist (lem, args)) + exact_no_check (applist (lem, args)) in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in Sigma.Unsafe.of_pair (tac, evd) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 47ff197a0..2ffedf81a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -114,7 +114,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic (** {6 Exact tactics. } *) val assumption : unit Proofview.tactic -val exact_no_check : constr -> tactic +val exact_no_check : constr -> unit Proofview.tactic val vm_cast_no_check : constr -> tactic val native_cast_no_check : constr -> tactic val exact_check : constr -> unit Proofview.tactic |