aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml40
-rw-r--r--plugins/funind/gen_principle.ml10
-rw-r--r--plugins/funind/indfun_common.ml24
-rw-r--r--plugins/funind/recdef.ml19
4 files changed, 55 insertions, 38 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4200854c2..b864b18887 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) =
refine to_refine g) ]
let find_rectype env sigma c =
- let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in
+ let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in
match EConstr.kind sigma t with
| Ind ind -> (t, l)
| Construct _ -> (t, l)
@@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
let new_ctxt, new_end_of_type =
decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
in
- let prove_new_hyp : tactic =
- tclTHEN
- (tclDO ctxt_size (Proofview.V82.of_tactic intro))
- (fun g ->
- let all_ids = pf_ids_of_hyps g in
- let new_ids, _ = list_chop ctxt_size all_ids in
- let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.type_of g to_refine in
- tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g)
+ let prove_new_hyp =
+ let open Tacticals.New in
+ let open Tacmach.New in
+ tclTHEN (tclDO ctxt_size intro)
+ (Proofview.Goal.enter (fun g ->
+ let all_ids = pf_ids_of_hyps g in
+ let new_ids, _ = list_chop ctxt_size all_ids in
+ let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
+ let evm, _ =
+ Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ to_refine
+ in
+ tclTHEN
+ (Proofview.Unsafe.tclEVARS evm)
+ (Proofview.V82.tactic (refine to_refine))))
in
let simpl_eq_tac =
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
- prove_new_hyp
+ (Proofview.V82.of_tactic prove_new_hyp)
in
(* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *)
(* str "removing an equation " ++ fnl ()++ *)
@@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
let prov_hid = pf_get_new_id hid g in
let c = mkApp (mkVar hid, args) in
let evm, _ = pf_apply Typing.type_of g c in
- tclTHENLIST
- [ Refiner.tclEVARS evm
- ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c)
- ; thin [hid]
- ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ]
+ let open Tacticals.New in
+ Proofview.V82.of_tactic
+ (tclTHENLIST
+ [ Proofview.Unsafe.tclEVARS evm
+ ; pose_proof (Name prov_hid) c
+ ; clear [hid]
+ ; rename_hyp [(prov_hid, hid)] ])
g)
(fun (*
if not then we are in a mutual function block
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c53dcc7edd..608155eb71 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
in
(* uctx was ignored before *)
- let hook = DeclareDef.Hook.make (hook new_principle_type) in
+ let hook = Declare.Hook.make (hook new_principle_type) in
(body, typ, univs, hook, sigma)
let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
let uctx = Evd.evar_universe_context sigma in
let entry = Declare.definition_entry ~univs ?types body in
let (_ : Names.GlobRef.t) =
- DeclareDef.declare_entry ~name:new_princ_name ~hook
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ Declare.declare_entry ~name:new_princ_name ~hook
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
~impargs:[] ~uctx entry
in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
Pp.(str "Body of Function must be given")
in
ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior)
~kind:Decls.Definition univs binders None body (Some rtype);
let evd, rev_pconstants =
List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
(None, evd, List.rev rev_pconstants)
| _ ->
ComFixpoint.do_fixpoint
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
fixpoint_exprl;
let evd, rev_pconstants =
List.fold_left
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e83fe56cc9..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,7 @@ open Names
open Pp
open Constr
open Libnames
-open Refiner
+open Tacmach
let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id)
let mk_rel_id = mk_prefix "R_"
@@ -395,7 +395,8 @@ let jmeq_refl () =
with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
- tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+ Proofview.V82.of_tactic
+ (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
@@ -427,15 +428,16 @@ let evaluable_of_global_reference r =
| _ -> assert false
let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
- tclREPEAT
- (List.fold_right
- (fun (eq, b) i ->
- tclORELSE
- (Proofview.V82.of_tactic
- ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
- i)
- (if rev then List.rev eqs else eqs)
- (tclFAIL 0 (mt ())))
+ let open Tacticals in
+ (tclREPEAT
+ (List.fold_right
+ (fun (eq, b) i ->
+ tclORELSE
+ (Proofview.V82.of_tactic
+ ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+ i)
+ (if rev then List.rev eqs else eqs)
+ (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
let decompose_lam_n sigma n =
if n < 0 then
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..9b2d9c4815 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
in
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
-let pf_type c tac gl =
- let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
- tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_type c tac =
+ let open Tacticals.New in
+ Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let evars, ty = Typing.type_of env sigma c in
+ tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
+
+let pf_type c tac =
+ Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
let pf_typel l tac =
let rec aux tys l =
@@ -1483,7 +1490,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
in
- let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+ let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
let lemma =
Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
in
@@ -1721,7 +1728,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
- let hook {DeclareDef.Hook.S.uctx; _} =
+ let hook {Declare.Hook.S.uctx; _} =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref =
declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1774,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
functional_ref
(EConstr.of_constr rec_arg_type)
relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
- (DeclareDef.Hook.make hook))
+ (Declare.Hook.make hook))
()
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:41:25 +0000