diff options
Diffstat (limited to 'contrib/funind')
| -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 |
4 files changed, 15 insertions, 18 deletions
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 |