summaryrefslogtreecommitdiff
path: root/contrib/funind/functional_principles_proofs.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /contrib/funind/functional_principles_proofs.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib/funind/functional_principles_proofs.ml')
-rw-r--r--contrib/funind/functional_principles_proofs.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 3d80bd00..bd335d30 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,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)) (Genarg.IntroIdentifier prov_id) t))
+ ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
[tclTHENLIST
[
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
in
(* observe_tac "rec hyp " *)
(tclTHENS
- (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+ (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
[
(* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
(* observe_tac "prove rec hyp" *)
@@ -571,7 +571,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 (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
thin [hid];
h_rename [prov_hid,hid]
] g
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
false
(true,5)
[Lazy.force refl_equal]
- [empty_transparent_state, Auto.Hint_db.empty]
+ [Auto.Hint_db.empty false]
)
)
)
@@ -1497,7 +1497,7 @@ let prove_principle_for_gen
(tclTHEN
(forward
(Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
- (Genarg.IntroIdentifier wf_thm_id)
+ (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
(mkApp (delayed_force well_founded,[|input_type;relation|])))
(
(* observe_tac *)
@@ -1561,7 +1561,7 @@ let prove_principle_for_gen
);
(* observe_tac "" *) (forward
(Some (prove_rec_arg_acc))
- (Genarg.IntroIdentifier acc_rec_arg_id)
+ (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
);
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));