summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml12
-rw-r--r--contrib/funind/g_indfun.ml414
-rw-r--r--contrib/funind/indfun.ml2
-rw-r--r--contrib/funind/invfun.ml10
-rw-r--r--contrib/funind/recdef.ml4
5 files changed, 16 insertions, 26 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)));
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index dae76f2d..d435f513 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -90,11 +90,6 @@ END
TACTIC EXTEND newfunind
["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
[
- let pat =
- match pat with
- | None -> IntroAnonymous
- | Some pat -> pat
- in
let c = match cl with
| [] -> assert false
| [c] -> c
@@ -106,11 +101,6 @@ END
TACTIC EXTEND snewfunind
["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
[
- let pat =
- match pat with
- | None -> IntroAnonymous
- | Some pat -> pat
- in
let c = match cl with
| [] -> assert false
| [c] -> c
@@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl =
tclTHEN
(Tactics.letin_tac None (Name idunsafe) cstr allClauses)
(tclTHENFIRST
- (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr))
+ (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr))
Tactics.reflexivity)
gl
@@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
fun gl ->
(functional_induction
true (applist (info.fname, List.rev !list_constr_largs))
- None IntroAnonymous) gl))
+ None None) gl))
nexttac)) ordered_info_list in
(* we try each (f t u v) until one does not fail *)
(* TODO: try also to mix functional schemes *)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a6cbb321..79ef0097 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -120,7 +120,7 @@ let functional_induction with_clean c princl pat =
princ_infos
args_as_induction_constr
princ'
- pat
+ (None,pat)
None)
subst_and_reduce
g
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 63d44916..f62d70ab 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -280,13 +280,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.map
(fun (_,_,br_type) ->
List.map
- (fun id -> Genarg.IntroIdentifier id)
+ (fun id -> dummy_loc, Genarg.IntroIdentifier id)
(generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
)
branches
in
(* before building the full intro pattern for the principle *)
- let pat = Genarg.IntroOrAndPattern intro_pats in
+ let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
let eq_ind = Coqlib.build_coq_eq () in
let eq_construct = mkConstruct((destInd eq_ind),1) in
(* The next to referencies will be used to find out which constructor to apply in each branch *)
@@ -297,7 +297,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
(* We get the identifiers of this branch *)
let this_branche_ids =
List.fold_right
- (fun pat acc ->
+ (fun (_,pat) acc ->
match pat with
| Genarg.IntroIdentifier id -> Idset.add id acc
| _ -> anomaly "Not an identifier"
@@ -447,7 +447,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
[ observe_tac "intro args_names" (tclMAP h_intro args_names);
observe_tac "principle" (forward
(Some (h_exact f_principle))
- (Genarg.IntroIdentifier principle_id)
+ (dummy_loc,Genarg.IntroIdentifier principle_id)
princ_type);
tclTHEN_i
(observe_tac "functional_induction" (
@@ -948,7 +948,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
thin [hid];
h_intro hid;
- Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+ Inv.inv FullInversion None (Rawterm.NamedHyp hid);
(fun g ->
let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index c9bf2f1f..5bd7a6b2 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Term
open Termops
@@ -1157,7 +1157,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 (IntroIdentifier heq2)
+ [forward None (dummy_loc,IntroIdentifier heq2)
(mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-14 20:41:21 +0000