diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/cc/cctac.ml | 8 | ||||
-rw-r--r-- | contrib/fourier/fourier.ml | 2 | ||||
-rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 19 | ||||
-rw-r--r-- | contrib/funind/g_indfun.ml4 | 2 | ||||
-rw-r--r-- | contrib/funind/invfun.ml | 8 | ||||
-rw-r--r-- | contrib/funind/recdef.ml | 4 | ||||
-rw-r--r-- | contrib/interface/depends.ml | 6 | ||||
-rw-r--r-- | contrib/interface/paths.ml | 2 | ||||
-rw-r--r-- | contrib/interface/pbp.ml | 2 | ||||
-rw-r--r-- | contrib/interface/showproof.ml | 3 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 16 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 2 |
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 |