aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml11
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/indfun.ml3
-rw-r--r--plugins/funind/invfun.ml15
-rw-r--r--plugins/funind/recdef.ml23
5 files changed, 37 insertions, 25 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 169a706005..f57f12f667 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -9,6 +9,7 @@ open Names
open Declarations
open Pp
open Tacmach
+open Termops
open Proof_type
open Tacticals
open Tactics
@@ -52,10 +53,10 @@ let rec print_debug_queue e =
let _ =
match e with
| Some e ->
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
| None ->
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
end in
print_debug_queue None ;
end
@@ -705,7 +706,7 @@ let build_proof
in
tclTHENSEQ
[
- Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
pattern_option [Locus.AllOccurrencesBut [1],t] None;
(fun g -> observe_tac "toto" (
@@ -932,7 +933,7 @@ let generalize_non_dep hyp g =
in
(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
tclTHEN
- ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) ))
+ ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) ))
((* observe_tac "thin" *) (thin to_revert))
g
@@ -1562,7 +1563,7 @@ let prove_principle_for_gen
Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
- tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l)
+ tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c47602bda0..bbe2f1a3ad 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -12,6 +12,7 @@ open Tactics
open Indfun_common
open Functional_principles_proofs
open Misctypes
+open Sigma.Notations
exception Toberemoved_with_rel of int*constr
exception Toberemoved
@@ -648,12 +649,15 @@ let build_case_scheme fa =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
in
- let ind_fun =
+ let (ind, sf) =
let ind = first_fun_kn,funs_indexes in
(ind,Univ.Instance.empty)(*FIXME*),prop_sort
in
- let sigma, scheme =
- (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma (scheme, sigma, _) =
+ Indrec.build_case_analysis_scheme_default env sigma ind sf
+ in
+ let sigma = Sigma.to_evar_map sigma in
let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dbd438061..bf9da870e4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,6 +10,7 @@ open Glob_term
open Declarations
open Misctypes
open Decl_kinds
+open Sigma.Notations
let is_rec_info scheme_info =
let test_branche min acc (_,_,br) =
@@ -85,7 +86,7 @@ let functional_induction with_clean c princl pat =
in
let encoded_pat_as_patlist =
List.make (List.length args + List.length c_list - 1) None @ [pat] in
- List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None))
+ List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
(args@c_list) encoded_pat_as_patlist
in
let princ' = Some (princ,bindings) in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d979401424..628e582e23 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,6 +19,7 @@ open Tactics
open Indfun_common
open Tacmach
open Misctypes
+open Termops
(* Some pretty printing function for debugging purpose *)
@@ -70,8 +71,8 @@ let do_observe_tac s tac g =
with reraise ->
let reraise = Errors.push reraise in
let e = Cerrors.process_vernac_interp_error reraise in
- observe (str "observation "++ s++str " raised exception " ++
- Errors.iprint e ++ str " on goal " ++ goal );
+ observe (hov 0 (str "observation "++ s++str " raised exception " ++
+ Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
iraise reraise;;
@@ -457,7 +458,7 @@ let generalize_dependent_of x hyp g =
tclMAP
(function
| (id,None,t) when not (Id.equal id hyp) &&
- (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id])
+ (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -698,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
})
Locusops.onConcl
;
- Simple.generalize (List.map mkVar ids);
+ generalize (List.map mkVar ids);
thin ids
]
else
@@ -737,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
tclTHENSEQ
[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
observe_tac "h_generalize"
- (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+ (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
Proofview.V82.of_tactic (Simple.intro graph_principle_id);
observe_tac "" (tclTHEN_i
(observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
@@ -920,7 +921,7 @@ let revert_graph kn post_tac hid g =
let f_args,res = Array.chop (Array.length args - 1) args in
tclTHENSEQ
[
- Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
post_tac hid
@@ -964,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
in
tclTHENSEQ[
pre_tac hid;
- Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+ generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 951bef2beb..5a30da336e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -29,6 +29,7 @@ open Proof_type
open Pfedit
open Glob_term
open Pretyping
+open Termops
open Constrintern
open Misctypes
open Genredexpr
@@ -38,6 +39,7 @@ open Auto
open Eauto
open Indfun_common
+open Sigma.Notations
@@ -212,10 +214,10 @@ let rec print_debug_queue b e =
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
else
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
end;
(* print_debug_queue false e; *)
end
@@ -685,11 +687,14 @@ let mkDestructEq :
to_revert_constr in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
- [Simple.generalize new_hyps;
+ [generalize new_hyps;
(fun g2 ->
- Proofview.V82.of_tactic (change_in_concl None
- (fun patvars sigma ->
- pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
+ let changefun patvars = { run = fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in
+ Sigma.Unsafe.of_pair (c, sigma)
+ } in
+ Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -1110,7 +1115,7 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id]))
+ tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))
))
;
observe_tac (str "fix") (fix (Some hrec) (nargs+1));
@@ -1300,7 +1305,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (str "")
[
- Simple.generalize [lemma];
+ generalize [lemma];
Proofview.V82.of_tactic (Simple.intro hid);
(fun g ->
let ids = pf_ids_of_hyps g in
@@ -1327,7 +1332,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
tclFIRST[
tclTHEN
(Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
- e_assumption;
+ (Proofview.V82.of_tactic e_assumption);
Eauto.eauto_with_bases
(true,5)
[Evd.empty,Lazy.force refl_equal]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:08:57 +0000