aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/fourier/fourierR.ml121
-rw-r--r--plugins/fourier/g_fourier.ml42
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml40
-rw-r--r--plugins/omega/coq_omega.ml2
-rw-r--r--plugins/romega/refl_omega.ml4
-rw-r--r--proofs/logic.ml1
-rw-r--r--tactics/eauto.ml46
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/equality.ml7
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/rewrite.ml12
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tactics.ml641
-rw-r--r--tactics/tactics.mli20
-rw-r--r--tactics/tauto.ml42
-rw-r--r--toplevel/auto_ind_decl.ml10
20 files changed, 484 insertions, 402 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index dbd89019e..e6a841153 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -248,7 +248,7 @@ module Btauto = struct
let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (Tactics.change_concl changed_gl);
- Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+ Tactics.apply (Lazy.force soundness);
Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
try_unification env
]
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 70aaa0c0f..3151a7ec7 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -486,7 +486,7 @@ let f_equal =
else
Tacticals.New.tclTRY (Tacticals.New.tclTHEN
((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
- (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c)))))
+ (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 7c134da7a..a77b1d60a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -377,10 +377,10 @@ let tac_zero_inf_pos gl (n,d) =
let tacn=ref (apply (get coq_Rlt_zero_1)) in
let tacd=ref (apply (get coq_Rlt_zero_1)) in
for _i = 1 to n - 1 do
- tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
+ tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
for _i = 1 to d - 1 do
- tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
- (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
+ tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+ (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
;;
(* preuve que 0<=n*1/d
@@ -391,10 +391,10 @@ let tac_zero_infeq_pos gl (n,d)=
else (apply (get coq_Rle_zero_1))) in
let tacd=ref (apply (get coq_Rlt_zero_1)) in
for _i = 1 to n - 1 do
- tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
+ tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
for _i = 1 to d - 1 do
- tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
- (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
+ tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+ (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
;;
(* preuve que 0<(-n)*(1/d) => False
@@ -402,14 +402,14 @@ let tac_zero_infeq_pos gl (n,d)=
let tac_zero_inf_false gl (n,d) =
if n=0 then (apply (get coq_Rnot_lt0))
else
- (tclTHEN (apply (get coq_Rle_not_lt))
+ (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
(tac_zero_infeq_pos gl (-n,d)))
;;
(* preuve que 0<=(-n)*(1/d) => False
*)
let tac_zero_infeq_false gl (n,d) =
- (tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
+ (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
(tac_zero_inf_pos gl (-n,d)))
;;
@@ -423,14 +423,14 @@ let my_cut c gl=
let exact = exact_check;;
let tac_use h =
- let tac = Proofview.V82.of_tactic (exact h.hname) in
+ let tac = exact h.hname in
match h.htype with
"Rlt" -> tac
|"Rle" -> tac
- |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
- |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
- |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
- |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
+ |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
+ |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
+ |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
+ |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
|_->assert false
;;
@@ -462,43 +462,44 @@ let mkAppL a =
exception GoalDone
(* Résolution d'inéquations linéaires dans R *)
-let rec fourier gl=
+let rec fourier () =
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
- let goal = strip_outer_cast (pf_concl gl) in
+ let goal = strip_outer_cast concl in
let fhyp=Id.of_string "new_hyp_for_fourier" in
(* si le but est une inéquation, on introduit son contraire,
et le but à prouver devient False *)
- try (let tac =
- match (kind_of_term goal) with
+ try
+ match (kind_of_term goal) with
App (f,args) ->
(match (string_of_R_constr f) with
"Rlt" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_ge_lt))
- (Proofview.V82.of_tactic (intro_using fhyp)))
- fourier)
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
+ (intro_using fhyp))
+ (fourier ()))
|"Rle" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_gt_le))
- (Proofview.V82.of_tactic (intro_using fhyp)))
- fourier)
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
+ (intro_using fhyp))
+ (fourier ()))
|"Rgt" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_le_gt))
- (Proofview.V82.of_tactic (intro_using fhyp)))
- fourier)
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
+ (intro_using fhyp))
+ (fourier ()))
|"Rge" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_lt_ge))
- (Proofview.V82.of_tactic (intro_using fhyp)))
- fourier)
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
+ (intro_using fhyp))
+ (fourier ()))
|_-> raise GoalDone)
|_-> raise GoalDone
- in tac gl)
with GoalDone ->
(* les hypothèses *)
let hyps = List.map (fun (h,t)-> (mkVar h,t))
- (list_of_sign (pf_hyps gl)) in
+ (list_of_sign (Proofview.Goal.hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
with NoIneq -> ())
@@ -506,7 +507,7 @@ let rec fourier gl=
(* lineq = les inéquations découlant des hypothèses *)
if !lineq=[] then Errors.error "No inequalities";
let res=fourier_lineq (!lineq) in
- let tac=ref tclIDTAC in
+ let tac=ref (Proofview.tclUNIT ()) in
if res=[]
then Errors.error "fourier failed"
(* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
@@ -551,11 +552,11 @@ let rec fourier gl=
let tc=rational_to_real cres in
(* puis sa preuve *)
let tac1=ref (if h1.hstrict
- then (tclTHENS (apply (get coq_Rfourier_lt))
+ then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
[tac_use h1;
tac_zero_inf_pos gl
(rational_to_fraction c1)])
- else (tclTHENS (apply (get coq_Rfourier_le))
+ else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
[tac_use h1;
tac_zero_inf_pos gl
(rational_to_fraction c1)])) in
@@ -563,20 +564,20 @@ let rec fourier gl=
List.iter (fun (h,c)->
(if (!s)
then (if h.hstrict
- then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt))
+ then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le))
+ else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)]))
else (if h.hstrict
- then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt))
+ then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le))
+ else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])));
@@ -586,43 +587,43 @@ let rec fourier gl=
then tac_zero_inf_false gl (rational_to_fraction cres)
else tac_zero_infeq_false gl (rational_to_fraction cres)
in
- tac:=(tclTHENS (my_cut ineq)
- [tclTHEN (change_concl
+ tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq))
+ [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl
(mkAppL [| get coq_not; ineq|]
- ))
- (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
+ )))
+ (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
else get coq_Rnot_le_le))
- (tclTHENS (Proofview.V82.of_tactic (Equality.replace
+ (Tacticals.New.tclTHENS (Equality.replace
(mkAppL [|get coq_Rminus;!t2;!t1|]
)
- tc))
+ tc)
[tac2;
- (tclTHENS
- (Proofview.V82.of_tactic (Equality.replace
+ (Tacticals.New.tclTHENS
+ (Equality.replace
(mkApp (get coq_Rinv,
[|get coq_R1|]))
- (get coq_R1)))
+ (get coq_R1))
(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
- [tclORELSE
- (* TODO : Ring.polynom []*) tclIDTAC
- tclIDTAC;
- pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
- (tclTHEN (apply symeq)
+ [Tacticals.New.tclORELSE
+ (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
+ (Proofview.tclUNIT ());
+ Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
+ (Tacticals.New.tclTHEN (apply symeq)
(apply (get coq_Rinv_1))))]
)
]));
!tac1]);
- tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False)))
- [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None));
+ tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
+ [Tacticals.New.tclTHEN intro (contradiction None);
!tac])
|_-> assert false) |_-> assert false
);
(* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
- (!tac gl)
+ !tac
(* ((tclABSTRACT None !tac) gl) *)
-
+ end
;;
(*
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 11107385d..25451fd92 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -13,5 +13,5 @@ open FourierR
DECLARE PLUGIN "fourier_plugin"
TACTIC EXTEND fourier
- [ "fourierz" ] -> [ Proofview.V82.tactic fourier ]
+ [ "fourierz" ] -> [ fourier () ]
END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1981fb837..7f0db547d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1433,11 +1433,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
backtrack_eqs_until_hrec hrec eqs;
(* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
(tclTHENS (* We must have exactly ONE subgoal !*)
- (apply (mkVar hrec))
+ (Proofview.V82.of_tactic (apply (mkVar hrec)))
[ tclTHENSEQ
[
keep (tcc_hyps@eqs);
- apply (Lazy.force acc_inv);
+ (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
(fun g ->
if is_mes
then
@@ -1556,7 +1556,7 @@ let prove_principle_for_gen
(
(* observe_tac *)
(* "apply wf_thm" *)
- Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
+ Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])))
)
)
)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5682c2aa4..4fcc65bda 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -487,7 +487,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
(fun gl ->
let term = mkApp (mkVar principle_id,Array.of_list bindings) in
let gl', _ty = pf_eapply Typing.e_type_of gl term in
- apply term gl')
+ Proofview.V82.of_tactic (apply term) gl')
))
(fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1fa16a301..ff35c9812 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -255,7 +255,7 @@ let tclUSER tac is_mes l g =
| None -> clear []
| Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
in
- tclTHENSEQ
+ tclTHENLIST
[
clear_tac;
if is_mes
@@ -271,7 +271,7 @@ let tclUSER tac is_mes l g =
let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
if is_mes
- then tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof))
+ then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
@@ -377,12 +377,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
) [] rev_context in
let rev_ids = pf_get_new_ids (List.rev ids) g in
let new_b = substl (List.map mkVar rev_ids) b in
- tclTHENSEQ
+ tclTHENLIST
[
h_intros (List.rev rev_ids);
Proofview.V82.of_tactic (intro_using teq_id);
onLastHypId (fun heq ->
- tclTHENSEQ[
+ tclTHENLIST[
thin to_intros;
h_intros to_intros;
(fun g' ->
@@ -507,14 +507,14 @@ let rec prove_lt hyple g =
let y =
List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
tclTHENLIST[
- apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]));
+ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
observe_tac (str "prove_lt") (prove_lt hyple)
]
with Not_found ->
(
(
tclTHENLIST[
- apply (delayed_force lt_S_n);
+ Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
(observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
])
)
@@ -764,7 +764,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
];
observe_tac (str "proving decreasing") (
tclTHENS (* proof of args < formal args *)
- (apply (Lazy.force expr_info.acc_inv))
+ (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
[
observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
tclTHENLIST
@@ -812,7 +812,7 @@ let rec prove_le g =
in
tclFIRST[
Proofview.V82.of_tactic assumption;
- apply (delayed_force le_n);
+ Proofview.V82.of_tactic (apply (delayed_force le_n));
begin
try
let matching_fun =
@@ -825,7 +825,7 @@ let rec prove_le g =
List.hd (List.tl args)
in
tclTHENLIST[
- apply(mkApp(le_trans (),[|x;y;z;mkVar h|]));
+ Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
observe_tac (str "prove_le (rec)") (prove_le)
]
with Not_found -> tclFAIL 0 (mt())
@@ -855,7 +855,7 @@ let rec make_rewrite_list expr_info max = function
)
[make_rewrite_list expr_info max l;
tclTHENLIST[ (* x < S max proof *)
- apply (delayed_force le_lt_n_Sm);
+ Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
observe_tac (str "prove_le(2)") prove_le
]
] )
@@ -892,7 +892,7 @@ let make_rewrite expr_info l hp max =
(observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))]))
;
tclTHENLIST[ (* x < S (S max) proof *)
- apply (delayed_force le_lt_SS);
+ Proofview.V82.of_tactic (apply (delayed_force le_lt_SS));
observe_tac (str "prove_le (3)") prove_le
]
])
@@ -1082,12 +1082,12 @@ let termination_proof_header is_mes input_type ids args_id relation
(* this gives the accessibility argument *)
observe_tac
(str "apply wf_thm")
- (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
+ (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
)
]
;
(* rest of the proof *)
- tclTHENSEQ
+ tclTHENLIST
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
@@ -1206,7 +1206,7 @@ let build_and_l l =
let c,tac,nb = f pl in
mk_and p1 c,
tclTHENS
- (apply (constr_of_global conj_constr))
+ (Proofview.V82.of_tactic (apply (constr_of_global conj_constr)))
[tclIDTAC;
tac
],nb+1
@@ -1278,7 +1278,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
build_proof Evd.empty_evar_universe_context
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
- tclTHENSEQ
+ tclTHENLIST
[
Simple.generalize [lemma];
Proofview.V82.of_tactic (Simple.intro hid);
@@ -1306,7 +1306,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
tclCOMPLETE(
tclFIRST[
tclTHEN
- (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+ (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
e_assumption;
Eauto.eauto_with_bases
(true,5)
@@ -1338,11 +1338,11 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
(tclFIRST
(List.map
(fun c ->
- tclTHENSEQ
- [Proofview.V82.of_tactic intros;
+ Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
+ [intros;
Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
- tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
- ]
+ Tacticals.New.tclCOMPLETE Auto.default_auto
+ ])
)
using_lemmas)
) tclIDTAC)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 271cade27..48c853029 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -37,7 +37,7 @@ let elim_id id =
Proofview.Goal.enter begin fun gl ->
simplest_elim (Tacmach.New.pf_global id gl)
end
-let resolve_id id gl = apply (pf_global gl id) gl
+let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
let timing timer_name f arg = f arg
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e22816c13..1835b6cc9 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1283,7 +1283,7 @@ let resolution env full_reified_goal systems_list =
Tactics.generalize
(l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
Tactics.change_concl reified >>
- Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
+ Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
show_goal >>
Tactics.normalise_vm_in_concl >>
(*i Alternatives to the previous line:
@@ -1292,7 +1292,7 @@ let resolution env full_reified_goal systems_list =
- Skip the conversion check and rely directly on the QED:
Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
i*)
- Tactics.apply (Lazy.force coq_I)
+ Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I))
let total_reflexive_omega_tactic gl =
Coqlib.check_required_library ["Coq";"romega";"ROmega"];
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59de85901..dc8f31859 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -573,6 +573,7 @@ let prim_refiner r sigma goal =
raise (RefinerError IntroNeedsProduct))
| Cut (b,replace,id,t) ->
+(* if !check && not (Retyping.get_sort_of env sigma t) then*)
let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
let sign,t,cl,sigma =
if replace then
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dbfde64e4..a4babd276 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -79,8 +79,8 @@ let apply_tac_list tac glls =
let one_step l gl =
[Proofview.V82.of_tactic Tactics.intro]
- @ (List.map Tactics.Simple.eapply (List.map mkVar (pf_ids_of_hyps gl)))
- @ (List.map Tactics.Simple.eapply l)
+ @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
+ @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
@ (List.map assumption (pf_ids_of_hyps gl))
let rec prolog l n gl =
@@ -122,7 +122,7 @@ let unify_e_resolve poly flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv' in
let clenv' = clenv_unique_resolver ~flags clenv' gls in
tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c)) gls
+ (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
let e_exact poly flags (c,clenv) =
let clenv', subst =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 5aceeb9f4..1c249c999 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -117,7 +117,7 @@ let diseqCase eqonleft =
(tclTHEN (choose_noteq eqonleft)
(tclTHEN (Proofview.V82.tactic red_in_concl)
(tclTHEN (intro_using absurd)
- (tclTHEN (Proofview.V82.tactic (Simple.apply (mkVar diseq)))
+ (tclTHEN (Simple.apply (mkVar diseq))
(tclTHEN (Extratactics.injHyp absurd)
(full_trivial [])))))))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 91d774e6e..56a5920a1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,7 +563,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
(clear [id]));
tclFIRST
[assumption;
- tclTHEN (Proofview.V82.tactic (apply sym)) assumption;
+ tclTHEN (apply sym) assumption;
try_prove_eq
]
]))
@@ -1513,9 +1513,8 @@ let cutSubstInHyp_LR eqn id =
let sigma,body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in
if not (dependent (mkRel 1) body) then raise NothingToRewrite;
let refine = Proofview.V82.tactic (fun gl -> Tacmach.refine_no_check (mkVar id) gl) in
- let subst = Proofview.V82.of_tactic (tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine) in
- Proofview.V82.tclEVARS sigma <*>
- Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl)
+ let subst = tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine in
+ Proofview.V82.tclEVARS sigma <*> (cut_replacing id expected_goal subst)
end
let cutSubstInHyp_RL eqn id =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index af28f5145..e50786b31 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -477,7 +477,7 @@ let step left x tac =
let l =
List.map (fun lem ->
Tacticals.New.tclTHENLAST
- (Proofview.V82.tactic (apply_with_bindings (lem, ImplicitBindings [x])))
+ (apply_with_bindings (lem, ImplicitBindings [x]))
tac)
!(if left then transitivity_left_table else transitivity_right_table)
in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8592cd33d..a8a4b1dcc 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1426,7 +1426,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
let tac =
match clause, p with
| Some id, Some p ->
- cut_replacing id newt (Tacmach.refine p)
+ Proofview.V82.of_tactic (cut_replacing id newt (Proofview.V82.tactic (Tacmach.refine p)))
| Some id, None ->
change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly)
| None, Some p ->
@@ -2025,7 +2025,7 @@ let setoid_reflexivity =
setoid_proof "reflexive"
(fun env evm car rel ->
tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof
- env evm car rel) apply)
+ env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c)))
(reflexivity_red true)
let setoid_symmetry =
@@ -2034,7 +2034,7 @@ let setoid_symmetry =
tac_open
(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
env evm car rel)
- apply)
+ (fun c -> Proofview.V82.of_tactic (apply c)))
(symmetry_red true)
let setoid_transitivity c =
@@ -2043,8 +2043,8 @@ let setoid_transitivity c =
tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
env evm car rel)
(fun proof -> match c with
- | None -> eapply proof
- | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
+ | None -> Proofview.V82.of_tactic (eapply proof)
+ | Some c -> Proofview.V82.of_tactic (apply_with_bindings (proof,ImplicitBindings [ c ]))))
(transitivity_red true c)
let setoid_symmetry_in id =
@@ -2063,7 +2063,7 @@ let setoid_symmetry_in id =
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
tclTHENS (Proofview.V82.of_tactic (Tactics.cut new_hyp))
[ intro_replacing id;
- tclTHENLIST [ Proofview.V82.of_tactic intros; Proofview.V82.of_tactic setoid_symmetry; apply (mkVar id); Proofview.V82.of_tactic Tactics.assumption ] ]
+ Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]) ]
gl)
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e1c53df4d..02e49584f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1691,7 +1691,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
in
let tac = match cl with
- | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
+ | None -> fun l -> Tactics.apply_with_bindings_gen a ev l
| Some cl ->
(fun l ->
Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59318fb22..c82db8531 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -182,25 +182,9 @@ let apply_clear_request clear_flag dft c =
if clear then Proofview.V82.tactic (thin [destVar c])
else Tacticals.New.tclIDTAC
-let internal_cut_gen b d t gl =
- try internal_cut b d t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_clear_dependency (pf_env gl) id err
-
-let internal_cut = internal_cut_gen false
-let internal_cut_replace = internal_cut_gen true
-
-let internal_cut_rev_gen b id t gl =
- try internal_cut_rev b id t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_clear_dependency (pf_env gl) id err
-
-let internal_cut_rev_replace = internal_cut_rev_gen true
-
(* Moving hypotheses *)
let move_hyp = Tacmach.move_hyp
-
(* Renaming hypotheses *)
let rename_hyp = Tacmach.rename_hyp
@@ -217,6 +201,71 @@ let fresh_id avoid id gl =
let new_fresh_id avoid id gl =
fresh_id_in_env avoid id (Proofview.Goal.env gl)
+let id_of_name_with_default id = function
+ | Anonymous -> id
+ | Name id -> id
+
+let default_id_of_sort s =
+ if Sorts.is_small s then default_small_ident else default_type_ident
+
+let default_id env sigma = function
+ | (name,None,t) ->
+ let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
+ id_of_name_with_default dft name
+ | (name,Some b,_) -> id_of_name_using_hdchar env b name
+
+(* Non primitive introduction tactics are treated by intro_then_gen
+ There is possibly renaming, with possibly names to avoid and
+ possibly a move to do after the introduction *)
+
+type name_flag =
+ | NamingAvoid of Id.t list
+ | NamingBasedOn of Id.t * Id.t list
+ | NamingMustBe of Loc.t * Id.t
+
+let find_name repl decl naming gl = match naming with
+ | NamingAvoid idl ->
+ (* this case must be compatible with [find_intro_names] below. *)
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ new_fresh_id idl (default_id env sigma decl) gl
+ | NamingBasedOn (id,idl) -> new_fresh_id idl id gl
+ | NamingMustBe (loc,id) ->
+ (* When name is given, we allow to hide a global name *)
+ let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
+ let id' = next_ident_away id ids_of_hyps in
+ if not repl && not (Id.equal id' id) then
+ user_err_loc (loc,"",pr_id id ++ str" is already used.");
+ id
+
+(**************************************************************)
+(* Cut rule *)
+(**************************************************************)
+
+let internal_cut_gen b naming t =
+ Proofview.Goal.raw_enter begin fun gl ->
+ try
+ let id = find_name b (Anonymous,None,t) naming gl in
+ Proofview.V82.tactic (internal_cut b id t)
+ with Evarutil.ClearDependencyError (id,err) ->
+ error_clear_dependency (Proofview.Goal.env gl) id err
+ end
+
+let internal_cut = internal_cut_gen false
+let internal_cut_replace = internal_cut_gen true
+
+let internal_cut_rev_gen b naming t =
+ Proofview.Goal.raw_enter begin fun gl ->
+ try
+ let id = find_name b (Anonymous,None,t) naming gl in
+ Proofview.V82.tactic (internal_cut_rev b id t)
+ with Evarutil.ClearDependencyError (id,err) ->
+ error_clear_dependency (Proofview.Goal.env gl) id err
+ end
+
+let internal_cut_rev = internal_cut_rev_gen false
+let internal_cut_rev_replace = internal_cut_rev_gen true
+
(**************************************************************)
(* Fixpoints and CoFixpoints *)
(**************************************************************)
@@ -462,42 +511,6 @@ let unfold_constr = function
(* Introduction tactics *)
(*******************************************)
-let id_of_name_with_default id = function
- | Anonymous -> id
- | Name id -> id
-
-let default_id_of_sort s =
- if Sorts.is_small s then default_small_ident else default_type_ident
-
-let default_id env sigma = function
- | (name,None,t) ->
- let dft = default_id_of_sort (Typing.sort_of env sigma t) in
- id_of_name_with_default dft name
- | (name,Some b,_) -> id_of_name_using_hdchar env b name
-
-(* Non primitive introduction tactics are treated by central_intro
- There is possibly renaming, with possibly names to avoid and
- possibly a move to do after the introduction *)
-
-type intro_name_flag =
- | IntroAvoid of Id.t list
- | IntroBasedOn of Id.t * Id.t list
- | IntroMustBe of Id.t
-
-let find_name loc decl x gl = match x with
- | IntroAvoid idl ->
- (* this case must be compatible with [find_intro_names] below. *)
- let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
- new_fresh_id idl (default_id env sigma decl) gl
- | IntroBasedOn (id,idl) -> new_fresh_id idl id gl
- | IntroMustBe id ->
- (* When name is given, we allow to hide a global name *)
- let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
- let id' = next_ident_away id ids_of_hyps in
- if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
- id'
-
(* Returns the names that would be created by intros, without doing
intros. This function is supposed to be compatible with an
iteration of [find_name] above. As [default_id] checks the sort of
@@ -518,16 +531,16 @@ let build_intro_tac id dest tac = match dest with
| MoveLast -> Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
| dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
-let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
+let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
Proofview.Goal.raw_enter begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let concl = nf_evar (Proofview.Goal.sigma gl) concl in
match kind_of_term concl with
| Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
- let name = find_name loc (name,None,t) name_flag gl in
+ let name = find_name false (name,None,t) name_flag gl in
build_intro_tac name move_flag tac
| LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
- let name = find_name loc (name,Some b,t) name_flag gl in
+ let name = find_name false (name,Some b,t) name_flag gl in
build_intro_tac name move_flag tac
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -539,23 +552,23 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
end <*>
Proofview.tclORELSE
(Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
- (intro_then_gen loc name_flag move_flag false dep_flag tac))
+ (intro_then_gen name_flag move_flag false dep_flag tac))
begin function
| RefinerError IntroNeedsProduct ->
- Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc)
+ Proofview.tclZERO (Errors.UserError("Intro",str "No product even after head-reduction."))
| e -> Proofview.tclZERO e
end
end
-let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ())
-let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
-let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) MoveLast false false
-let intro_then = intro_then_gen dloc (IntroAvoid []) MoveLast false false
-let intro = intro_gen dloc (IntroAvoid []) MoveLast false false
-let introf = intro_gen dloc (IntroAvoid []) MoveLast true false
-let intro_avoiding l = intro_gen dloc (IntroAvoid l) MoveLast false false
+let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
+let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false
+let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
+let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
+let intro = intro_gen (NamingAvoid []) MoveLast false false
+let introf = intro_gen (NamingAvoid []) MoveLast true false
+let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
-let intro_then_force = intro_then_gen dloc (IntroAvoid []) MoveLast true false
+let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
(**** Multiple introduction tactics ****)
@@ -565,13 +578,13 @@ let rec intros_using = function
let intros = Tacticals.New.tclREPEAT intro
-let intro_forthcoming_then_gen loc name_flag move_flag dep_flag n bound tac =
+let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
let rec aux n ids =
(* Note: we always use the bound when there is one for "*" and "**" *)
if (match bound with None -> true | Some (_,p) -> n < p) then
Proofview.tclORELSE
begin
- intro_then_gen loc name_flag move_flag false dep_flag
+ intro_then_gen name_flag move_flag false dep_flag
(fun id -> aux (n+1) (id::ids))
end
begin function
@@ -625,8 +638,8 @@ let intros_replacing ids =
(* User-level introduction tactics *)
let intro_move idopt hto = match idopt with
- | None -> intro_gen dloc (IntroAvoid []) hto true false
- | Some id -> intro_gen dloc (IntroMustBe id) hto true false
+ | None -> intro_gen (NamingAvoid []) hto true false
+ | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
let pf_lookup_hypothesis_as_renamed env ccl = function
| AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n
@@ -691,7 +704,7 @@ let try_intros_until tac = function
let rec intros_move = function
| [] -> Proofview.tclUNIT ()
| (hyp,destopt) :: rest ->
- Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false)
+ Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false)
(intros_move rest)
(* Apply a tactic on a quantified hypothesis, an hypothesis in context
@@ -775,7 +788,9 @@ let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
another hypothesis.
*)
-let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
+let assert_replacing id t tac =
+ Tacticals.New.tclTHENFIRST
+ (internal_cut_replace (NamingMustBe (dloc,id)) t) tac
(* [cut_replacing id T tac] adds the subgoals of the proof of [T]
after the current goal
@@ -788,7 +803,9 @@ let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
another hypothesis.
*)
-let cut_replacing id t tac = tclTHENLAST (internal_cut_rev_replace id t) tac
+let cut_replacing id t tac =
+ Tacticals.New.tclTHENLAST
+ (internal_cut_rev_replace (NamingMustBe (dloc,id)) t) tac
let error_uninstantiated_metas t clenv =
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
@@ -808,10 +825,9 @@ let check_unresolved_evars_of_metas sigma clenv =
| _ -> ())
(meta_list clenv.evd)
-let clear_of_flag flag =
- match flag with
- | None -> true (* default for apply in *)
- | Some b -> b
+let make_naming id t = function
+ | None -> (true,NamingMustBe (dloc,id)) (* default for apply in *)
+ | Some naming -> naming
(* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
@@ -819,8 +835,7 @@ let clear_of_flag flag =
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv0 gl =
- let with_clear = clear_of_flag clear_flag in
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 =
let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv0 in
let clenv =
if with_classes then
@@ -832,15 +847,16 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clea
if not with_evars && occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
- let id' = if with_clear then id else fresh_id [] id gl in
- let exact_tac = refine_no_check new_hyp_prf in
- tclTHEN
- (tclEVARS clenv.evd)
+ let exact_tac = Proofview.V82.tactic (refine_no_check new_hyp_prf) in
+ let with_clear,naming = make_naming id new_hyp_prf naming in
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tclEVARS clenv.evd)
(if sidecond_first then
- tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac
+ Tacticals.New.tclTHENFIRST
+ (internal_cut_gen with_clear naming new_hyp_typ) exact_tac
else
- tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac)
- gl
+ Tacticals.New.tclTHENLAST
+ (internal_cut_rev_gen with_clear naming new_hyp_typ) exact_tac)
(********************************************)
(* Elimination tactics *)
@@ -894,19 +910,24 @@ let enforce_prop_bound_names rename tac =
| LetIn (na,c,t,t') ->
mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
| _ -> print_int i; Pp.msg (print_constr t); assert false in
- let rename_branch i gl =
- let env = pf_env gl in
- let sigma = project gl in
- let t = pf_concl gl in
- change_concl (aux env sigma i t) gl in
- (if isrec then tclTHENFIRSTn else tclTHENLASTn)
+ let rename_branch i =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let t = Proofview.Goal.concl gl in
+ Proofview.V82.tactic (fun gl -> change_concl (aux env sigma i t) gl)
+ end in
+ (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
tac
(Array.map rename_branch nn)
| _ ->
tac
-let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause gl =
- let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
+let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv =
(match kind_of_term (nth_arg i elimclause.templval.rebus) with
| Meta mv -> mv
@@ -914,7 +935,8 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim,
(str "The type of elimination clause is not well-formed."))
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- enforce_prop_bound_names rename (Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)) gl
+ enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)
+ end
(*
* Elimination tactic with bindings and using an arbitrary
@@ -930,48 +952,58 @@ type eliminator = {
elimbody : constr with_bindings
}
-let general_elim_clause_gen elimtac indclause elim gl =
+let general_elim_clause_gen elimtac indclause elim =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let (elimc,lbindelimc) = elim.elimbody in
- let elimt = pf_type_of gl elimc in
+ let elimt = Retyping.get_type_of env sigma elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
- elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
+ elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
+ end
-let general_elim with_evars clear_flag (c, lbindc) elim gl =
- let ct = pf_type_of gl c in
- let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
+let general_elim with_evars clear_flag (c, lbindc) elim =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let ct = Retyping.get_type_of env sigma c in
+ let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
let elimtac = elimination_clause_scheme with_evars in
- let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in
- tclTHEN
+ let indclause = make_clenv_binding env sigma (c, t) lbindc in
+ Tacticals.New.tclTHEN
(general_elim_clause_gen elimtac indclause elim)
- (Proofview.V82.of_tactic
- (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
- gl
+ (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
+ end
(* Case analysis tactics *)
-let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl =
- let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
- let sort = elimination_sort_of_goal gl in
+let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let concl = Proofview.Goal.concl gl in
+ let t = Retyping.get_type_of env sigma c in
+ let (mind,_) = reduce_to_quantified_ind env sigma t in
+ let sort = Tacticals.New.elimination_sort_of_goal gl in
let sigma, elim =
- if occur_term c (pf_concl gl) then
- pf_apply build_case_analysis_scheme gl mind true sort
+ if occur_term c concl then
+ build_case_analysis_scheme env sigma mind true sort
else
- pf_apply build_case_analysis_scheme_default gl mind sort in
- tclTHEN (tclEVARS sigma)
+ build_case_analysis_scheme_default env sigma mind sort in
+ Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
(general_elim with_evars clear_flag (c,lbindc)
{elimindex = None; elimbody = (elim,NoBindings);
- elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
+ elimrename = Some (false, constructors_nrealdecls (fst mind))})
+ end
let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
match kind_of_term c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
- (Proofview.V82.tactic
- (general_case_analysis_in_context with_evars clear_flag cx))
+ (general_case_analysis_in_context with_evars clear_flag cx)
| _ ->
- Proofview.V82.tactic
- (general_case_analysis_in_context with_evars clear_flag cx)
+ general_case_analysis_in_context with_evars clear_flag cx
let simplest_case c = general_case_analysis false None (c,NoBindings)
@@ -999,7 +1031,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
(Proofview.Goal.raw_enter begin fun gl ->
let evd, elim = find_eliminator c gl in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
- (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim))
+ (general_elim with_evars clear_flag cx elim)
end)
begin function
| IsRecord ->
@@ -1011,9 +1043,8 @@ let default_elim with_evars clear_flag (c,_ as cx) =
let elim_in_context with_evars clear_flag c = function
| Some elim ->
- Proofview.V82.tactic
- (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim;
- elimrename = None})
+ general_elim with_evars clear_flag c
+ {elimindex = Some (-1); elimbody = elim; elimrename = None}
| None -> default_elim with_evars clear_flag c
let elim with_evars clear_flag (c,lbindc as cx) elim =
@@ -1044,8 +1075,11 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
(* Set the hypothesis name in the message *)
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause gl =
- let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
let hypmv =
try match List.remove Int.equal indmv (clenv_independent elimclause) with
@@ -1055,21 +1089,22 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
(str "The type of elimination clause is not well-formed.") in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
let hyp = mkVar id in
- let hyp_typ = pf_type_of gl hyp in
- let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
+ let hyp_typ = Retyping.get_type_of env sigma hyp in
+ let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
if eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
- clenv_refine_in with_evars None id elimclause'' gl
+ clenv_refine_in with_evars None id elimclause''
+ end
let general_elim_clause with_evars flags id c e =
let elim = match id with
| None -> elimination_clause_scheme with_evars ~flags
| Some id -> elimination_in_clause_scheme with_evars ~flags id
in
- Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl)
+ general_elim_clause_gen elim c e
(* Apply a tactic below the products of the conclusion of a lemma *)
@@ -1114,100 +1149,143 @@ let make_projection env sigma params cstr sign elim i n c u =
| None -> None
in elim
-let descend_in_conjunctions tac exit c gl =
+let descend_in_conjunctions tac exit c =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
try
- let ((ind,u),t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let t = Retyping.get_type_of env sigma c in
+ let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
let sign,ccl = decompose_prod_assum t in
match match_with_tuple ccl with
| Some (_,_,isrec) ->
let n = (constructors_nrealargs ind).(0) in
- let sort = elimination_sort_of_goal gl in
- let id = fresh_id [] (Id.of_string "H") gl in
- let IndType (indf,_) = pf_apply find_rectype gl ccl in
+ let sort = Tacticals.New.elimination_sort_of_goal gl in
+ let IndType (indf,_) = find_rectype env sigma ccl in
let (_,inst), params = dest_ind_family indf in
- let cstr = (get_constructors (pf_env gl) indf).(0) in
+ let cstr = (get_constructors env indf).(0) in
let elim =
try DefinedRecord (Recordops.lookup_projections ind)
with Not_found ->
- let elim = pf_apply build_case_analysis_scheme gl (ind,u) false sort in
+ let elim = build_case_analysis_scheme env sigma (ind,u) false sort in
NotADefinedRecordUseScheme (snd elim) in
- tclFIRST
- (List.init n (fun i gl ->
- match pf_apply make_projection gl params cstr sign elim i n c u with
- | None -> tclFAIL 0 (mt()) gl
+ Tacticals.New.tclFIRST
+ (List.init n (fun i ->
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ match make_projection env sigma params cstr sign elim i n c u with
+ | None -> Tacticals.New.tclFAIL 0 (mt())
| Some (p,pt) ->
- tclTHENS
- (internal_cut id pt)
- [refine p; (* Might be ill-typed due to forbidden elimination. *)
- tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl))
- gl
+ Tacticals.New.tclTHENS
+ (internal_cut (NamingAvoid []) pt)
+ [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *)
+ Tacticals.New.onLastHypId (fun id ->
+ Tacticals.New.tclTHEN
+ (tac (not isrec) (mkVar id))
+ (Proofview.V82.tactic (thin [id])))]
+ end))
| None ->
raise Exit
with RefinerError _|UserError _|Exit -> exit ()
+ end
(****************************************************)
(* Resolution tactics *)
(****************************************************)
-let solve_remaining_apply_goals gl =
+let solve_remaining_apply_goals =
+ Proofview.Goal.enter begin fun gl ->
if !apply_solve_class_goals then
try
- let env = pf_env gl and sigma = project gl and concl = pf_concl gl in
- if Typeclasses.is_class_type sigma concl then
- let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in
- (tclTHEN (tclEVARS evd') (refine_no_check c')) gl
- else tclIDTAC gl
- with Not_found -> tclIDTAC gl
- else tclIDTAC gl
-
-let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 =
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let concl = Proofview.Goal.concl gl in
+ if Typeclasses.is_class_type sigma concl then
+ let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tclEVARS evd')
+ (Proofview.V82.tactic (refine_no_check c'))
+ else Proofview.tclUNIT ()
+ with Not_found -> Proofview.tclUNIT ()
+ else Proofview.tclUNIT ()
+ end
+
+let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
- let concl_nprod = nb_prod (pf_concl gl0) in
- let rec try_main_apply with_destruct c gl =
- let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
+ let concl_nprod = nb_prod concl in
+ let rec try_main_apply with_destruct c =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+
+ let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
let try_apply thm_ty nprod =
- let n = nb_prod thm_ty - nprod in
- if n<0 then error "Applied theorem has not enough premisses.";
- let clause = pf_apply make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
- Proofview.V82.of_tactic (Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags) gl
+ try
+ let n = nb_prod thm_ty - nprod in
+ if n<0 then error "Applied theorem has not enough premisses.";
+ let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
+ Clenvtac.res_pf clause ~with_evars ~flags
+ with UserError _ as exn ->
+ Proofview.tclZERO exn
in
- try try_apply thm_ty0 concl_nprod
- with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
+ Proofview.tclORELSE
+ (try_apply thm_ty0 concl_nprod)
+ (function PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
let rec try_red_apply thm_ty =
- try
+ try
(* Try to head-reduce the conclusion of the theorem *)
- let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
- try try_apply red_thm concl_nprod
- with PretypeError _|RefinerError _|UserError _|Failure _ ->
+ let red_thm = try_red_product env sigma thm_ty in
+ Proofview.tclORELSE
+ (try_apply red_thm concl_nprod)
+ (function PretypeError _|RefinerError _|UserError _|Failure _ ->
try_red_apply red_thm
- with Redelimination ->
+ | exn -> raise exn)
+ with Redelimination ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
- try if not (Int.equal concl_nprod 0) then try_apply thm_ty 0 else raise Exit
- with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
+ let tac =
if with_destruct then
descend_in_conjunctions
- try_main_apply (fun _ -> Loc.raise loc exn) c gl
+ try_main_apply
+ (fun _ -> Proofview.tclZERO (Loc.add_loc exn0 loc)) c
else
- Loc.raise loc exn
+ Proofview.tclZERO (Loc.add_loc exn0 loc) in
+ if not (Int.equal concl_nprod 0) then
+ try
+ Proofview.tclORELSE
+ (try_apply thm_ty 0)
+ (function PretypeError _|RefinerError _|UserError _|Failure _->
+ tac
+ | exn -> raise exn)
+ with UserError _ | Exit ->
+ tac
+ else
+ tac
in try_red_apply thm_ty0
+ | exn -> raise exn)
+ end
in
- tclTHENLIST [
+ Tacticals.New.tclTHENLIST [
try_main_apply with_destruct c;
solve_remaining_apply_goals;
- Proofview.V82.of_tactic
- (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
- ] gl0
+ apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
+ ]
+ end
let rec apply_with_bindings_gen b e = function
- | [] -> tclIDTAC
+ | [] -> Proofview.tclUNIT ()
| [k,cb] -> general_apply b b e k cb
| (k,cb)::cbl ->
- tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl)
+ Tacticals.New.tclTHENLAST
+ (general_apply b b e k cb)
+ (apply_with_bindings_gen b e cbl)
let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
@@ -1249,8 +1327,8 @@ let progress_with_clause flags innerclause clause =
try List.find_map f ordered_metas
with Not_found -> error "Unable to unify."
-let apply_in_once_main flags innerclause (d,lbind) gl =
- let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
+let apply_in_once_main flags innerclause env sigma (d,lbind) =
+ let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
let rec aux clause =
try progress_with_clause flags innerclause clause
with e when Errors.noncritical e ->
@@ -1258,26 +1336,32 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
try aux (clenv_push_prod clause)
with NotExtensibleClause -> raise e
in
- aux (pf_apply make_clenv_binding gl (d,thm) lbind)
+ aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag
- id (clear_flag,(loc,(d,lbind))) gl0 =
+let apply_in_once sidecond_first with_delta with_destruct with_evars naming
+ id (clear_flag,(loc,(d,lbind))) =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
- let t' = pf_get_hyp_typ gl0 id in
- let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
- let rec aux with_destruct c gl =
+ let t' = Tacmach.New.pf_get_hyp_typ id gl in
+ let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
+ let rec aux with_destruct c =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
try
- let clause = apply_in_once_main flags innerclause (c,lbind) gl in
- tclTHEN
- (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause)
- (Proofview.V82.of_tactic
- (apply_clear_request clear_flag false c))
- gl
+ let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
+ Tacticals.New.tclTHEN
+ (clenv_refine_in ~sidecond_first with_evars naming id clause)
+ (apply_clear_request clear_flag false c)
with e when with_destruct ->
let e = Errors.push e in
- descend_in_conjunctions aux (fun _ -> raise e) c gl
+ descend_in_conjunctions aux (fun _ -> raise e) c
+ end
in
- aux with_destruct d gl0
+ aux with_destruct d
+ end
(* A useful resolution tactic which, if c:A->B, transforms |- C into
|- B -> C and |- A
@@ -1436,7 +1520,7 @@ let specialize (c,lbind) g =
| Var id when Id.List.mem id (pf_ids_of_hyps g) ->
tclTHEN tac
(tclTHENFIRST
- (fun g -> internal_cut_replace id (pf_type_of g term) g)
+ (fun g -> Proofview.V82.of_tactic (internal_cut_replace (NamingMustBe (dloc,id)) (pf_type_of g term)) g)
(exact_no_check term)) g
| _ -> tclTHEN tac
(tclTHENLAST
@@ -1487,7 +1571,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
(Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in
let cons = mkConstructU cons in
- let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in
+ let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
(Tacticals.New.tclTHENLIST
[Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
end
@@ -1500,7 +1584,7 @@ let one_constructor i lbind = constructor_tac false None i lbind
*)
let rec tclANY tac = function
-| [] -> Proofview.tclZERO (Errors.UserError ("", str "No applicable tactic."))
+| [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.")
| arg :: l ->
Proofview.tclOR (tac arg) (fun _ -> tclANY tac l)
@@ -1618,7 +1702,7 @@ let rewrite_hyp l2r id =
else
Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
| _ ->
- Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
+ Tacticals.New.tclZEROMSG (str"Cannot find a known equation.")
end
let rec explicit_intro_names = function
@@ -1664,31 +1748,31 @@ let rec intros_patterns b avoid ids thin destopt bound n tac = function
| [] when fit_bound n bound -> tac ids thin
| [] ->
(* Behave as IntroAnonymous *)
- intro_then_gen dloc (IntroAvoid avoid)
+ intro_then_gen (NamingAvoid avoid)
destopt true false
(fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac [])
| (loc,pat) :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
match pat with
| IntroWildcard ->
- intro_then_gen loc (IntroBasedOn(wild_id,avoid@explicit_intro_names l))
+ intro_then_gen (NamingBasedOn(wild_id,avoid@explicit_intro_names l))
MoveLast true false
(fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt bound (n+1) tac l)
| IntroIdentifier id ->
check_thin_clash_then id thin avoid (fun thin ->
- intro_then_gen loc (IntroMustBe id) destopt true false
+ intro_then_gen (NamingMustBe (loc,id)) destopt true false
(fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l))
| IntroAnonymous ->
- intro_then_gen loc (IntroAvoid (avoid@explicit_intro_names l))
+ intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt true false
(fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
- intro_then_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l))
+ intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
destopt true false
(fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
| IntroForthcoming onlydeps ->
- intro_forthcoming_then_gen loc (IntroAvoid (avoid@explicit_intro_names l))
+ intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt onlydeps n bound
(fun ids -> intros_patterns b avoid ids thin destopt bound (n+List.length ids) tac l)
| IntroOrAndPattern ll ->
@@ -1700,7 +1784,7 @@ let rec intros_patterns b avoid ids thin destopt bound n tac = function
(intro_decomp_eq loc l' thin
(fun thin bound' -> intros_patterns b avoid ids thin destopt bound' 0 (fun ids thin -> intros_patterns b avoid ids thin destopt bound (n+1) tac l)))
| IntroRewrite l2r ->
- intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
+ intro_then_gen (NamingAvoid(avoid@explicit_intro_names l))
MoveLast true false
(fun id ->
Tacticals.New.tclTHENLAST (* Skip the side conditions of the rewriting step *)
@@ -1733,63 +1817,64 @@ let intro_patterns = function
(* Other cut tactics *)
(**************************)
-let make_id s = new_fresh_id [] (default_id_of_sort s)
-
-let prepare_intros s ipat gl =
- let make_id s = make_id s gl in
- let fresh_id l id = new_fresh_id l id gl in
- match ipat with
- | None ->
- make_id s , Proofview.tclUNIT ()
- | Some (loc,ipat) -> match ipat with
- | IntroIdentifier id ->
- id, Proofview.tclUNIT ()
- | IntroAnonymous ->
- make_id s , Proofview.tclUNIT ()
- | IntroFresh id ->
- fresh_id [] id , Proofview.tclUNIT ()
+let rec prepare_naming loc = function
+ | IntroIdentifier id -> NamingMustBe (loc,id)
+ | IntroAnonymous -> NamingAvoid []
+ | IntroFresh id -> NamingBasedOn (id,[])
| IntroWildcard ->
- let id = make_id s in
- id , clear_wildcards [dloc,id]
+ error "Did you really mind erasing the newly generated hypothesis?"
+ | IntroRewrite _
+ | IntroOrAndPattern _
+ | IntroInjection _
+ | IntroForthcoming _ -> assert false
+
+let rec prepare_intros_loc loc dft = function
+ | IntroIdentifier _
+ | IntroAnonymous
+ | IntroFresh _
+ | IntroWildcard as ipat ->
+ prepare_naming loc ipat,
+ (fun _ -> Proofview.tclUNIT ())
| IntroRewrite l2r ->
- let id = make_id s in
- id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+ prepare_naming loc dft,
+ (fun id -> Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl)
| IntroOrAndPattern ll ->
- make_id s,
- Tacticals.New.onLastHypId
- (intro_or_and_pattern loc true ll []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l)))
+ prepare_naming loc dft,
+ (intro_or_and_pattern loc true ll []
+ (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
+ (fun _ l -> clear_wildcards l)))
| IntroInjection l ->
- make_id s,
- Tacticals.New.onLastHypId
- (intro_decomp_eq loc l []
- (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l)))
+ prepare_naming loc dft,
+ (intro_decomp_eq loc l []
+ (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
+ (fun _ l -> clear_wildcards l)))
| IntroForthcoming _ -> user_err_loc
- (loc,"",str "Introduction pattern for one hypothesis expected")
+ (loc,"",str "Introduction pattern for one hypothesis expected.")
+
+let prepare_intros dft = function
+ | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
+ | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
let ipat_of_name = function
| Anonymous -> None
| Name id -> Some (dloc, IntroIdentifier id)
-let allow_replace c = function (* A rather arbitrary condition... *)
- | Some (_, IntroIdentifier id) ->
- let c = fst (decompose_app ((strip_lam_assum c))) in
- if isVar c && Id.equal (destVar c) id then Some id else None
- | _ ->
- None
+ let head_ident c =
+ let c = fst (decompose_app ((strip_lam_assum c))) in
+ if isVar c then Some (destVar c) else None
+
+let do_replace id = function
+ | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
+ | _ -> false
let assert_as first ipat c =
- Proofview.Goal.raw_enter begin fun gl ->
- let hnf_type_of = Tacmach.New.pf_hnf_type_of gl in
- match kind_of_term (hnf_type_of c) with
- | Sort s ->
- let (id,tac) = prepare_intros s ipat gl in
- let repl = not (Option.is_empty (allow_replace c ipat)) in
- Tacticals.New.tclTHENS
- (Proofview.V82.tactic ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c))
- (if first then [Proofview.tclUNIT (); tac] else [tac; Proofview.tclUNIT ()])
- | _ -> Proofview.tclZERO (Errors.UserError ("",str"Not a proposition or a type."))
- end
+ let naming,tac = prepare_intros IntroAnonymous ipat in
+ let repl = do_replace (head_ident c) naming in
+ Tacticals.New.tclTHENS
+ ((if first then internal_cut_gen
+ else internal_cut_rev_gen) repl naming c)
+ (if first then [Proofview.tclUNIT (); Tacticals.New.onLastHypId tac]
+ else [Tacticals.New.onLastHypId tac; Proofview.tclUNIT ()])
let assert_tac na = assert_as true (ipat_of_name na)
let enough_tac na = assert_as false (ipat_of_name na)
@@ -1814,28 +1899,27 @@ let as_tac id ipat = match ipat with
| None -> Proofview.tclUNIT ()
let tclMAPLAST tacfun l =
- let tacfun x = Proofview.V82.tactic (tacfun x) in
List.fold_right (fun x -> Tacticals.New.tclTHENLAST (tacfun x)) l (Proofview.tclUNIT())
let tclMAPFIRST tacfun l =
- let tacfun x = Proofview.V82.tactic (tacfun x) in
List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
let general_apply_in sidecond_first with_delta with_destruct with_evars
with_clear id lemmas ipat =
+ let tac (naming,lemma) =
+ apply_in_once sidecond_first with_delta with_destruct with_evars
+ naming id lemma in
+ let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+ let clear = do_replace (Some id) naming in
+ let lemmas_target =
+ let last,first = List.sep_last lemmas in
+ List.map (fun lem -> (None,lem)) first @ [(Some (clear,naming),last)]
+ in
if sidecond_first then
(* Skip the side conditions of the applied lemma *)
- Tacticals.New.tclTHENLAST
- (tclMAPLAST
- (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
- lemmas)
- (as_tac id ipat)
+ Tacticals.New.tclTHENLAST (tclMAPLAST tac lemmas_target) (ipat_tac id)
else
- Tacticals.New.tclTHENFIRST
- (tclMAPFIRST
- (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
- lemmas)
- (as_tac id ipat)
+ Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
let apply_in simple with_evars clear_flag id lemmas ipat =
general_apply_in false simple simple with_evars clear_flag id lemmas ipat
@@ -1888,7 +1972,7 @@ let letin_tac_gen with_eq abs ty =
let sigma, _ = Typing.e_type_of env sigma term in
sigma, term,
Tacticals.New.tclTHEN
- (intro_gen loc (IntroMustBe heq) (decode_hyp lastlhyp) true false)
+ (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
(Proofview.V82.tactic (thin_body [heq;id]))
| None ->
(Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
@@ -1899,7 +1983,7 @@ let letin_tac_gen with_eq abs ty =
Tacticals.New.tclTHENLIST
[ Proofview.V82.tclEVARS sigma;
Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
- intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false;
+ intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
eq_tac ]))
end
@@ -3333,7 +3417,8 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind in
let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
let elimc = mkCast (elimc, DEFAULTcast, elimt) in
- elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
+ Proofview.V82.of_tactic
+ (elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause) gl
let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
inhyps =
@@ -3376,7 +3461,7 @@ let induction_without_atomization isrec with_evars elim names lid =
in
let nlid = List.length lid in
if not (Int.equal nlid awaited_nargs)
- then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments."))
+ then Tacticals.New.tclZEROMSG (str"Not the right number of induction arguments.")
else
Proofview.tclTHEN (Proofview.V82.tclEVARS sigma)
(induction_from_context_l with_evars elim_info lid names)
@@ -3691,11 +3776,9 @@ let symmetry_red allowred =
match_with_equation concl >>= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
- Proofview.V82.tactic begin
- tclTHEN
- (convert_concl_no_check concl DEFAULTcast)
- (pf_constr_of_global eq_data.sym apply)
- end
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+ (Tacticals.New.pf_constr_of_global eq_data.sym apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
end
@@ -3723,7 +3806,7 @@ let symmetry_in id =
| HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
[ Proofview.V82.tactic (intro_replacing id);
- Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ]
+ Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
end
begin function
| NoEquationFound -> Hook.get forward_setoid_symmetry_in id
@@ -3785,16 +3868,14 @@ let transitivity_red allowred t =
match_with_equation concl >>= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
- Proofview.V82.tactic begin
- tclTHEN
- (convert_concl_no_check concl DEFAULTcast)
- (match t with
- | None -> pf_constr_of_global eq_data.trans eapply
- | Some t -> pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
- end
- | None,eq,eq_kind ->
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+ (match t with
+ | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
+ | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+ | None,eq,eq_kind ->
match t with
- | None -> Proofview.tclZERO (Errors.UserError ("",str"etransitivity not supported for this relation."))
+ | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
| Some t -> prove_transitivity eq eq_kind t
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f58e218be..f50e52a19 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -175,14 +175,14 @@ val revert : Id.t list -> unit Proofview.tactic
val apply_type : constr -> constr list -> tactic
val bring_hyps : named_context -> unit Proofview.tactic
-val apply : constr -> tactic
-val eapply : constr -> tactic
+val apply : constr -> unit Proofview.tactic
+val eapply : constr -> unit Proofview.tactic
val apply_with_bindings_gen :
- advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> tactic
+ advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic
-val apply_with_bindings : constr with_bindings -> tactic
-val eapply_with_bindings : constr with_bindings -> tactic
+val apply_with_bindings : constr with_bindings -> unit Proofview.tactic
+val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic
val cut_and_apply : constr -> unit Proofview.tactic
@@ -251,7 +251,7 @@ type eliminator = {
}
val general_elim : evars_flag -> clear_flag ->
- constr with_bindings -> eliminator -> tactic
+ constr with_bindings -> eliminator -> unit Proofview.tactic
val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
clausenv -> eliminator -> unit Proofview.tactic
@@ -336,8 +336,8 @@ val intros_transitivity : constr option -> unit Proofview.tactic
val cut : constr -> unit Proofview.tactic
val cut_intro : constr -> unit Proofview.tactic
-val assert_replacing : Id.t -> types -> tactic -> tactic
-val cut_replacing : Id.t -> types -> tactic -> tactic
+val assert_replacing : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
+val cut_replacing : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
val forward : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
@@ -386,8 +386,8 @@ module Simple : sig
val generalize : constr list -> tactic
val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic
- val apply : constr -> tactic
- val eapply : constr -> tactic
+ val apply : constr -> unit Proofview.tactic
+ val eapply : constr -> unit Proofview.tactic
val elim : constr -> unit Proofview.tactic
val case : constr -> unit Proofview.tactic
val apply_in : identifier -> constr -> unit Proofview.tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d972fb929..8d040c257 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -314,7 +314,7 @@ let coq_nnpp_path =
let tauto_classical flags nnpp =
Proofview.tclORELSE
- (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply nnpp)) (tauto_intuitionistic flags))
+ (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
begin function
| UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
| e -> Proofview.tclZERO e
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 15b370b06..c3dc8f89d 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -387,7 +387,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
in
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
- Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
+ Equality.replace p q ; apply app ; Auto.default_auto]
end
(* used in the bool -> leib side *)
@@ -456,7 +456,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
Equality.replace_by t1 t2
- (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply app)) (Auto.default_auto)) ;
+ (Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ;
aux q1 q2 ]
)
)
@@ -727,7 +727,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
intros; (Proofview.V82.tactic simpl_in_concl);
Auto.default_auto;
Tacticals.New.tclREPEAT (
- Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
+ Tacticals.New.tclTHENLIST [apply (andb_true_intro());
simplest_split ;Auto.default_auto ]
);
Proofview.Goal.enter begin fun gls ->
@@ -892,7 +892,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
(* left *)
Tacticals.New.tclTHENLIST [
simplest_left;
- Proofview.V82.tactic (apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)));
+ apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
Auto.default_auto
]
;
@@ -908,7 +908,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
assert_by (Name freshH3)
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
(Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)));
+ apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
Auto.default_auto
]);
Equality.general_rewrite_bindings_in true
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 06:49:31 +0000