aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/recdef.ml14
-rw-r--r--plugins/omega/coq_omega.ml46
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/setoid_ring/newring.ml4
8 files changed, 43 insertions, 43 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 5a49fc8f4..57eb80f5f 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 e676a8a93..d539eda57 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 4eab5f912..aa89f89b7 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 0c9d3bb81..ae2091a22 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 b09678341..834d0acea 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 7e38109d6..ad63c90f2 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 560e6a899..177c870b3 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 ed6db90d6..a67cc7cb8 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)));;
(****************************************************************************)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:13:35 +0000