diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 20 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 17 | ||||
| -rw-r--r-- | tactics/eqschemes.mli | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 |
5 files changed, 25 insertions, 24 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e6a8cbe3ad..8a6d93cf7c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in - (c, Evd.evar_universe_context sigma), Declareops.no_seff + (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0a..b2603315d5 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -193,7 +193,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Declareops.no_seff) + (c, ctx), Safe_typing.empty_private_constants) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff + in (c, Evd.evar_universe_context_of ctx), + Safe_typing.concat_private eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -704,7 +705,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) (* End of rewriting schemes *) @@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 6bb84808a9..3fe3307308 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val build_r2l_forward_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index bc711b81ef..674c85af79 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = assert false in let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Declareops.no_seff + sigma, elim, Safe_typing.empty_private_constants else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1437b24625..0b920066fd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac = (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in - let open Declareops in - let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = |