aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml16
-rw-r--r--plugins/funind/functional_principles_types.ml13
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml13
-rw-r--r--plugins/funind/invfun.ml15
-rw-r--r--plugins/funind/merge.ml19
-rw-r--r--plugins/funind/recdef.ml25
8 files changed, 58 insertions, 49 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 169a706005..4eab5f9126 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -3,12 +3,12 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Declarations
open Pp
open Tacmach
+open Termops
open Proof_type
open Tacticals
open Tactics
@@ -52,10 +52,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
@@ -229,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
+let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
let nochange ?t' msg =
begin
observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
@@ -705,7 +705,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 +932,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
@@ -1472,7 +1472,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
tclCOMPLETE(
Eauto.eauto_with_bases
(true,5)
- [Evd.empty,Lazy.force refl_equal]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
)
)
@@ -1562,7 +1562,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..e2c3bbb978 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -3,7 +3,6 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Pp
@@ -12,6 +11,7 @@ open Tactics
open Indfun_common
open Functional_principles_proofs
open Misctypes
+open Sigma.Notations
exception Toberemoved_with_rel of int*constr
exception Toberemoved
@@ -29,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let env = Global.env () in
let env_with_params = Environ.push_rel_context princ_type_info.params env in
let tbl = Hashtbl.create 792 in
- let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context =
+ let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t =
match predicates with
| [] -> []
|(Name x,v,t)::predicates ->
@@ -648,12 +648,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/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index a15e46bfe3..97b9e95e10 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -55,7 +55,9 @@ let pr_with_bindings_typed prc prlc (c,bl) =
let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it)
+ | Some b ->
+ let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
+ spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
ARGUMENT EXTEND fun_ind_using
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5d92fca5ea..80de8e764d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
let new_env = add_pat_variables env pat typ in
let res =
fst (
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,v,t) (env,ctxt) ->
match na with
| Anonymous -> assert false
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dbd438061..d1e1098259 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
@@ -727,9 +728,9 @@ let rec add_args id new_args b =
List.map (fun (e,o) -> add_args id new_args e,o) bl)
| CCases(loc,sty,b_option,cel,cal) ->
CCases(loc,sty,Option.map (add_args id new_args) b_option,
- List.map (fun (b,(na,b_option)) ->
+ List.map (fun (b,na,b_option) ->
add_args id new_args b,
- (na, b_option)) cel,
+ na, b_option) cel,
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
@@ -751,10 +752,8 @@ let rec add_args id new_args b =
| CCast(loc,b1,b2) ->
CCast(loc,add_args id new_args b1,
Miscops.map_cast_type (add_args id new_args) b2)
- | CRecord (loc, w, pars) ->
- CRecord (loc,
- (match w with Some w -> Some (add_args id new_args w) | _ -> None),
- List.map (fun (e,o) -> e, add_args id new_args o) pars)
+ | CRecord (loc, pars) ->
+ CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars)
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
| CPrim _ -> b
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index a800c186af..0c9d3bb819 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/merge.ml b/plugins/funind/merge.ml
index 87d7ca76d7..57782dd71f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Declarations
open Glob_term
@@ -258,27 +257,27 @@ type merge_infos =
lnk2: int merged_arg array;
(** rec params which remain rec param (ie not linked) *)
- recprms1: rel_declaration list;
- recprms2: rel_declaration list;
+ recprms1: Context.Rel.Declaration.t list;
+ recprms2: Context.Rel.Declaration.t list;
nrecprms1: int;
nrecprms2: int;
(** rec parms which became non parm (either linked to something
or because after a rec parm that became non parm) *)
- otherprms1: rel_declaration list;
- otherprms2: rel_declaration list;
+ otherprms1: Context.Rel.Declaration.t list;
+ otherprms2: Context.Rel.Declaration.t list;
notherprms1:int;
notherprms2:int;
(** args which remain args in merge *)
- args1:rel_declaration list;
- args2:rel_declaration list;
+ args1:Context.Rel.Declaration.t list;
+ args2:Context.Rel.Declaration.t list;
nargs1:int;
nargs2:int;
(** functional result args *)
- funresprms1: rel_declaration list;
- funresprms2: rel_declaration list;
+ funresprms1: Context.Rel.Declaration.t list;
+ funresprms2: Context.Rel.Declaration.t list;
nfunresprms1:int;
nfunresprms2:int;
}
@@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
lident , bindlist , Some cstr_expr , lcstor_expr
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 065d0fe537..b096783412 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,10 +1332,10 @@ 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]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
]
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:03:04 +0000