diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 5a49fc8f452b..57eb80f5fbc9 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -250,7 +250,7 @@ module Btauto = struct Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; Tactics.apply (Lazy.force soundness); - Proofview.V82.tactic (Tactics.normalise_vm_in_concl); + Tactics.normalise_vm_in_concl; try_unification env ] | _ -> diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index e676a8a9365f..d539eda5799d 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -210,6 +210,6 @@ let defined_connectives=lazy let normalize_evaluables= onAllHypsAndConcl (function - None->unfold_in_concl (Lazy.force defined_connectives) + None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) | Some id -> - unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4eab5f912699..aa89f89b74d3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1334,7 +1334,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]; + [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); let do_prove = build_proof interactive_proof @@ -1460,7 +1460,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb81993..ae2091a227c1 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -484,15 +484,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -703,7 +703,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = thin ids ] else - unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))] + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]) in (* The proof of each branche itself *) let ind_number = ref 0 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b09678341217..834d0aceac8b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -276,8 +276,8 @@ let tclUSER tac is_mes l g = if is_mes then observe_tclTHENLIST (str "tclUSER2") [ - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference - (delayed_force Indfun_common.ltof_ref))]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference + (delayed_force Indfun_common.ltof_ref))]); tac ] else tac @@ -564,8 +564,8 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = h_intros [k;h';def]; observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference infos.func)]); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference infos.func)])); ( observe_tclTHENLIST (str "test")[ list_rewrite true @@ -904,8 +904,8 @@ let make_rewrite expr_info l hp max = (observe_tclTHENLIST (str "make_rewrite")[ simpl_iter Locusops.onConcl; observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference expr_info.func)]); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference expr_info.func)])); (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); @@ -1425,7 +1425,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]); observe_tac (str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 7e38109d67db..ad63c90f27d6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -927,15 +927,15 @@ let rec transform p t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - unfold sp_Zminus :: tac,t + Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t | Kapp(Zsucc,[t1]) -> let tac,t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in - unfold sp_Zsucc :: tac,t + Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t | Kapp(Zpred,[t1]) -> let tac,t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in - unfold sp_Zpred :: tac,t + Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t | Kapp(Zmult,[t1;t2]) -> let tac1,t1' = transform (P_APP 1 :: p) t1 and tac2,t2' = transform (P_APP 2 :: p) t2 in @@ -1091,8 +1091,8 @@ let replay_history tactic_normalisation = in Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zle); - Proofview.V82.tactic (simpl_in_concl); + unfold sp_Zle; + simpl_in_concl; intro; (absurd not_sup_sup) ]) [ assumption ; reflexivity ] @@ -1135,10 +1135,10 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - (Proofview.V82.tactic (unfold sp_Zgt)); - (Proofview.V82.tactic simpl_in_concl); + (unfold sp_Zgt); + simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ] + Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] @@ -1160,18 +1160,18 @@ let replay_history tactic_normalisation = [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); Proofview.V82.tactic (clear [aux1;aux2]); - Proofview.V82.tactic (unfold sp_not); + unfold sp_not; (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); Proofview.V82.tactic (mk_then tac); assumption ] ; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ] | EXACT_DIVIDE (e1,k) :: l -> let id = hyp_of_tag e1.id in @@ -1208,8 +1208,8 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> @@ -1329,12 +1329,12 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl @@ -1343,9 +1343,9 @@ let replay_history tactic_normalisation = | CONSTANT_NEG(e,k) :: l -> Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]); - Proofview.V82.tactic (unfold sp_Zle); - Proofview.V82.tactic simpl_in_concl; - Proofview.V82.tactic (unfold sp_not); + unfold sp_Zle; + simpl_in_concl; + unfold sp_not; (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); reflexivity @@ -1839,7 +1839,7 @@ let destructure_goal = match destructurate_prop t with | Kapp(Not,[t]) -> (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro) + (Tacticals.New.tclTHEN (unfold sp_not) intro) destructure_hyps) | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 560e6a899eb5..177c870b3c0c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list = Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Tactics.normalise_vm_in_concl >> + Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index ed6db90d6309..a67cc7cb87f0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -99,10 +99,10 @@ let protect_red map env sigma c = (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));; (****************************************************************************) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c9b2c7cfde63..3ac3daef9ac3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -245,7 +245,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) - | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) + | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]))) | Extern tacast -> conclPattern concl p tacast in let tac = Proofview.V82.of_tactic (run_hint t tac) in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 6117c8b4326a..ae85f02d5991 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -503,7 +503,7 @@ let autounfolds db occs cls gl = let ids = Idset.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in unfold_option unfolds cls gl + in Proofview.V82.of_tactic (unfold_option unfolds cls) gl let autounfold db cls gl = let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index be4b135974c2..7c821ddcb52f 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -123,7 +123,7 @@ let diseqCase hyps eqonleft = (tclTHEN (intro_using diseq) (tclTHEN (choose_noteq eqonleft) (tclTHEN (rewrite_and_clear (List.rev hyps)) - (tclTHEN (Proofview.V82.tactic red_in_concl) + (tclTHEN (red_in_concl) (tclTHEN (intro_using absurd) (tclTHEN (Simple.apply (mkVar diseq)) (tclTHEN (Extratactics.injHyp absurd) diff --git a/tactics/equality.ml b/tactics/equality.ml index 1e814e861c9a..c9ecc55d1879 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1622,8 +1622,8 @@ let unfold_body x = let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in - let reducth h = Proofview.V82.tactic (fun gl -> reduct_in_hyp rfun h gl) in - let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in + let reducth h = reduct_in_hyp rfun h in + let reductc = reduct_in_concl (rfun, DEFAULTcast) in tclTHENLIST [tclMAP reducth hl; reductc] end end } diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d0a090e5c155..8b71affffa0b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1569,10 +1569,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = convert_concl_no_check newt DEFAULTcast in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in + let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in let opt_beta = match clause with | None -> Proofview.tclUNIT () - | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) + | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp) in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f76f4f6e2034..28d3ed18a1c9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -470,7 +470,7 @@ let cofix ido gl = match ido with type tactic_reduction = env -> evar_map -> constr -> constr let pf_reduce_decl redfun where (id,c,ty) gl = - let redfun' = Tacmach.pf_reduce redfun gl in + let redfun' = Tacmach.New.pf_apply redfun gl in match c with | None -> if where == InHypValueOnly then @@ -549,12 +549,15 @@ let bind_red_expr_occurrences occs nbcl redexp = reduction function either to the conclusion or to a certain hypothesis *) -let reduct_in_concl (redfun,sty) gl = - Proofview.V82.of_tactic (convert_concl_no_check (Tacmach.pf_reduce redfun gl (Tacmach.pf_concl gl)) sty) gl +let reduct_in_concl (redfun,sty) = + Proofview.Goal.nf_enter { enter = begin fun gl -> + convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty + end } -let reduct_in_hyp ?(check=false) redfun (id,where) gl = - Proofview.V82.of_tactic (convert_hyp ~check - (pf_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl)) gl +let reduct_in_hyp ?(check=false) redfun (id,where) = + Proofview.Goal.nf_enter { enter = begin fun gl -> + convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl) + end } let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -798,7 +801,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = else Proofview.tclUNIT () end <*> Proofview.tclORELSE - (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl) + (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> @@ -2728,8 +2731,8 @@ let unfold_body x gl = let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in tclTHENLIST - [tclMAP (fun h -> reduct_in_hyp rfun h) hl; - reduct_in_concl (rfun,DEFAULTcast)] gl + [tclMAP (fun h -> Proofview.V82.of_tactic (reduct_in_hyp rfun h)) hl; + Proofview.V82.of_tactic (reduct_in_concl (rfun,DEFAULTcast))] gl (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id]) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5564b61c372d..657367e36c88 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -128,38 +128,38 @@ type tactic_reduction = env -> evar_map -> constr -> constr type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg -val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic -val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic -val reduct_in_concl : tactic_reduction * cast_kind -> tactic +val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic +val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic +val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> hyp_location -> unit Proofview.tactic -val red_in_concl : tactic -val red_in_hyp : hyp_location -> tactic -val red_option : goal_location -> tactic -val hnf_in_concl : tactic -val hnf_in_hyp : hyp_location -> tactic -val hnf_option : goal_location -> tactic -val simpl_in_concl : tactic -val simpl_in_hyp : hyp_location -> tactic -val simpl_option : goal_location -> tactic -val normalise_in_concl : tactic -val normalise_in_hyp : hyp_location -> tactic -val normalise_option : goal_location -> tactic -val normalise_vm_in_concl : tactic +val red_in_concl : unit Proofview.tactic +val red_in_hyp : hyp_location -> unit Proofview.tactic +val red_option : goal_location -> unit Proofview.tactic +val hnf_in_concl : unit Proofview.tactic +val hnf_in_hyp : hyp_location -> unit Proofview.tactic +val hnf_option : goal_location -> unit Proofview.tactic +val simpl_in_concl : unit Proofview.tactic +val simpl_in_hyp : hyp_location -> unit Proofview.tactic +val simpl_option : goal_location -> unit Proofview.tactic +val normalise_in_concl : unit Proofview.tactic +val normalise_in_hyp : hyp_location -> unit Proofview.tactic +val normalise_option : goal_location -> unit Proofview.tactic +val normalise_vm_in_concl : unit Proofview.tactic val unfold_in_concl : - (occurrences * evaluable_global_reference) list -> tactic + (occurrences * evaluable_global_reference) list -> unit Proofview.tactic val unfold_in_hyp : - (occurrences * evaluable_global_reference) list -> hyp_location -> tactic + (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic val unfold_option : - (occurrences * evaluable_global_reference) list -> goal_location -> tactic + (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : constr_pattern option -> change_arg -> clause -> tactic val pattern_option : (occurrences * constr) list -> goal_location -> tactic val reduce : red_expr -> clause -> tactic -val unfold_constr : global_reference -> tactic +val unfold_constr : global_reference -> unit Proofview.tactic (** {6 Modification of the local context. } *) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f0c7a396135d..c143243b1d32 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -580,7 +580,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTRY ( Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); - Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp)); + simpl_in_hyp (freshz,Locus.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) @@ -724,7 +724,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj None false None (mkVar freshz,NoBindings); - intros; (Proofview.V82.tactic simpl_in_concl); + intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [apply (andb_true_intro()); @@ -901,7 +901,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; - Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref)); + unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all (); assert_by (Name freshH3)