aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/cc/cctac.ml8
-rw-r--r--contrib/fourier/fourier.ml2
-rw-r--r--contrib/funind/functional_principles_proofs.ml19
-rw-r--r--contrib/funind/g_indfun.ml42
-rw-r--r--contrib/funind/invfun.ml8
-rw-r--r--contrib/funind/recdef.ml4
-rw-r--r--contrib/interface/depends.ml6
-rw-r--r--contrib/interface/paths.ml2
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/showproof.ml3
-rw-r--r--contrib/interface/xlate.ml16
-rw-r--r--contrib/subtac/subtac_utils.ml2
12 files changed, 37 insertions, 37 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d2df855ee..dcd0ea469 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -317,7 +317,7 @@ let refute_tac c t1 t2 p gls =
[|intype;tt1;tt2|]) in
let hid=pf_get_new_id (id_of_string "Heq") gls in
let false_t=mkApp (c,[|mkVar hid|]) in
- tclTHENS (true_cut (Name hid) neweq)
+ tclTHENS (assert_tac (Name hid) neweq)
[proof_tac p; simplest_elim false_t] gls
let convert_to_goal_tac c t1 t2 p gls =
@@ -329,14 +329,14 @@ let convert_to_goal_tac c t1 t2 p gls =
let identity=mkLambda (Name x,sort,mkRel 1) in
let endt=mkApp (Lazy.force _eq_rect,
[|sort;tt1;identity;c;tt2;mkVar e|]) in
- tclTHENS (true_cut (Name e) neweq)
+ tclTHENS (assert_tac (Name e) neweq)
[proof_tac p;exact_check endt] gls
let convert_to_hyp_tac c1 t1 c2 t2 p gls =
let tt2=constr_of_term t2 in
let h=pf_get_new_id (id_of_string "H") gls in
let false_t=mkApp (c2,[|mkVar h|]) in
- tclTHENS (true_cut (Name h) tt2)
+ tclTHENS (assert_tac (Name h) tt2)
[convert_to_goal_tac c1 t1 t2 p;
simplest_elim false_t] gls
@@ -358,7 +358,7 @@ let discriminate_tac cstr p gls =
let endt=mkApp (Lazy.force _eq_rect,
[|outtype;trivial;pred;identity;concl;injt|]) in
let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
- tclTHENS (true_cut (Name hid) neweq)
+ tclTHENS (assert_tac (Name hid) neweq)
[proof_tac p;exact_check endt] gls
(* wrap everything *)
diff --git a/contrib/fourier/fourier.ml b/contrib/fourier/fourier.ml
index afd85de0a..dd54aea29 100644
--- a/contrib/fourier/fourier.ml
+++ b/contrib/fourier/fourier.ml
@@ -202,4 +202,4 @@ let test2=[
deduce test2;;
unsolvable test2;;
-*) \ No newline at end of file
+*)
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 903136ca2..52543cea1 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -153,7 +153,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
fun g ->
let prov_id = pf_get_new_id hyp_id g in
tclTHENS
- ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
+ ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
[tclTHENLIST
[
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -429,7 +429,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
in
(* observe_tac "rec hyp " *)
(tclTHENS
- (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
+ (assert_tac (Name rec_pte_id) t_x)
[
(* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
(* observe_tac "prove rec hyp" *)
@@ -618,7 +618,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
fun g ->
let prov_hid = pf_get_new_id hid g in
tclTHENLIST[
- forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
thin [hid];
h_rename [prov_hid,hid]
] g
@@ -1546,10 +1546,9 @@ let prove_principle_for_gen
((* observe_tac "prove_rec_arg_acc" *)
(tclCOMPLETE
(tclTHEN
- (forward
- (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
- (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
- (mkApp (delayed_force well_founded,[|input_type;relation|])))
+ (assert_by (Name wf_thm_id)
+ (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
(
(* observe_tac *)
(* "apply wf_thm" *)
@@ -1610,10 +1609,10 @@ let prove_principle_for_gen
(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
- (* observe_tac "" *) (forward
- (Some (prove_rec_arg_acc))
- (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
+ (* observe_tac "" *) (assert_by
+ (Name acc_rec_arg_id)
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ (prove_rec_arg_acc)
);
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index 654474b32..a79b46d96 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -358,7 +358,7 @@ let poseq_unsafe idunsafe cstr gl =
tclTHEN
(Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
(tclTHENFIRST
- (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr))
+ (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
Tactics.reflexivity)
gl
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index f62d70ab9..5c8f08715 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -445,10 +445,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
in
tclTHENSEQ
[ observe_tac "intro args_names" (tclMAP h_intro args_names);
- observe_tac "principle" (forward
- (Some (h_exact f_principle))
- (dummy_loc,Genarg.IntroIdentifier principle_id)
- princ_type);
+ observe_tac "principle" (assert_by
+ (Name principle_id)
+ princ_type
+ (h_exact f_principle));
tclTHEN_i
(observe_tac "functional_induction" (
fun g ->
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 528c276c0..100868a0e 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation
(observe_tac
"first assert"
(assert_tac
- true (* the assert thm is in first subgoal *)
(Name wf_rec_arg)
(mkApp (delayed_force acc_rel,
[|input_type;relation;mkVar rec_arg_id|])
@@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation
(observe_tac
"second assert"
(assert_tac
- true
(Name wf_thm)
(mkApp (delayed_force well_founded,[|input_type;relation|]))
)
@@ -1155,7 +1153,7 @@ let rec introduce_all_values_eq cont_tac functional termine
[] ->
let heq2 = next_global_ident_away true heq_id ids in
tclTHENLIST
- [forward None (dummy_loc,IntroIdentifier heq2)
+ [pose_proof (Name heq2)
(mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3d..e59de34a4 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -67,6 +67,7 @@ let explore_tree pfs =
| Move (bool, identifier, identifier') -> "Move"
| Rename (identifier, identifier') -> "Rename"
| Change_evars -> "Change_evars"
+ | Order _ -> "Order"
in
let pt = proof_of_pftreestate pfs in
(* We expect 0 *)
@@ -280,8 +281,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacExact c
| TacExactNoCheck c
| TacVmCastNoCheck c -> depends_of_'constr c acc
- | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
- | TacApply (_, _, _) -> failwith "TODO"
+ | TacApply (_, _, [cb], None) -> depends_of_'constr_with_bindings cb acc
+ | TacApply (_, _, _, _) -> failwith "TODO"
| TacElim (_, cwb, cwbo) ->
depends_of_'constr_with_bindings cwb
(Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -420,6 +421,7 @@ and depends_of_prim_rule pr acc = match pr with
| Move _ -> acc
| Rename _ -> acc
| Change_evars -> acc
+ | Order _ -> acc
let rec depends_of_pftree pt acc =
match pt.ref with
diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
index b1244d158..a157ca925 100644
--- a/contrib/interface/paths.ml
+++ b/contrib/interface/paths.ml
@@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with
[], _ -> true
| a::tl1, b::tl2 when a < b -> true
| a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;; \ No newline at end of file
+| _ -> false;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 65eadf13d..01747aa58 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
| PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
| PbpIntros l -> TacAtom (zz, TacIntroPattern l)
| PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
- | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
+ | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None))
| PbpElim (hyp_name, names) ->
let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4b9c1332a..cf861642d 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,8 @@ let rec natural_ntree ig ntree =
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
- | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
+ | TacApply (_,false,[c,_],None) ->
+ natural_apply ig lh g gs (snd c) ltree
| TacExact c -> natural_exact ig lh g gs (snd c) ltree
| TacCut c -> natural_cut ig lh g gs (snd c) ltree
| TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8ec6cfb2f..b404478ff 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1163,12 +1163,12 @@ and xlate_tac =
xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
- | TacApply (true,false,[c,bindl]) ->
+ | TacApply (true,false,[c,bindl],None) ->
CT_apply (xlate_formula c, xlate_bindings bindl)
- | TacApply (true,true,[c,bindl]) ->
+ | TacApply (true,true,[c,bindl],None) ->
CT_eapply (xlate_formula c, xlate_bindings bindl)
- | TacApply (_,_,_) ->
- xlate_error "TODO: simple (e)apply and iterated apply"
+ | TacApply (_,_,_,_) ->
+ xlate_error "TODO: simple (e)apply and iterated apply and apply in"
| TacConstructor (false,n_or_meta, bindl) ->
let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1256,13 +1256,13 @@ and xlate_tac =
but the structures are different *)
xlate_clause cl)
| TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
- | TacAssert (None, (_,IntroIdentifier id), c) ->
+ | TacAssert (None, Some (_,IntroIdentifier id), c) ->
CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (None, (_,IntroAnonymous), c) ->
+ | TacAssert (None, None, c) ->
CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
- | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) ->
+ | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) ->
CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (Some (TacId []), (_,IntroAnonymous), c) ->
+ | TacAssert (Some (TacId []), None, c) ->
CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
| TacAssert _ ->
xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 920b33b7a..4079b0f20 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
trace (spc () ++ str ("treating evar " ^ string_of_id n));
(try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
with _ -> ());
- let tac = assert_tac true (Name n) hyptype in
+ let tac = assert_tac (Name n) hyptype in
let conttac =
(fun cont ->
conttac
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-08 01:49:33 +0000