aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml5
-rw-r--r--tactics/elimschemes.ml26
-rw-r--r--tactics/elimschemes.mli2
-rw-r--r--tactics/eqschemes.ml16
-rw-r--r--tactics/eqschemes.mli4
-rw-r--r--tactics/ind_tables.ml16
-rw-r--r--tactics/ind_tables.mli10
7 files changed, 39 insertions, 40 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e91fe5067c..967b0ef418 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
(* do not compute the implicit arguments, it may be costly *)
let () = Impargs.make_implicit_args false in
(* ppedrot: seems legit to have abstracted subproofs as local*)
- Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
+ Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
in
let cst, eff = Impargs.with_implicit_protection cst () in
let inst = match const.Entries.const_entry_universes with
@@ -173,8 +173,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
in
let lem = mkConstU (cst, inst) in
let evd = Evd.set_universe_context evd ectx in
- let open Safe_typing in
- let effs = concat_private eff
+ let effs = Evd.concat_side_effects eff
Entries.(snd (Future.force const.const_entry_body)) in
let solve =
Proofview.tclEFFECTS effs <*>
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 8ead050262..06449c38a8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
else
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
- (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
+ (c, Evd.evar_universe_context sigma), Evd.empty_side_effects
let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
@@ -62,15 +62,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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects)
let rec_scheme_kind_from_type =
declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
@@ -90,7 +90,7 @@ let ind_scheme_kind_from_type =
let sind_scheme_kind_from_type =
declare_individual_scheme_object "_sind_nodep"
- (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
let ind_dep_scheme_kind_from_type =
declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
@@ -98,7 +98,7 @@ let ind_dep_scheme_kind_from_type =
let sind_dep_scheme_kind_from_type =
declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
- (fun _ x -> build_induction_scheme_in_type true InSProp x, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects)
let ind_scheme_kind_from_prop =
declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
@@ -106,7 +106,7 @@ let ind_scheme_kind_from_prop =
let sind_scheme_kind_from_prop =
declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
- (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+ (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
let nondep_elim_scheme from_kind to_kind =
match from_kind, to_kind with
@@ -130,24 +130,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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
let case_dep_scheme_kind_from_prop =
declare_individual_scheme_object "_case_dep"
- (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
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, Safe_typing.empty_private_constants)
+ (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index f60e6c137a..2b8a053cc0 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -18,7 +18,7 @@ val optimize_non_type_induction_scheme :
Sorts.family ->
'b ->
Names.inductive ->
- (Constr.constr * UState.t) * Safe_typing.private_constants
+ (Constr.constr * UState.t) * Evd.side_effects
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 3fdd97616f..d66ae9cb24 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -229,7 +229,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), Safe_typing.empty_private_constants)
+ (c, ctx), Evd.empty_side_effects)
(**********************************************************************)
(* Build the involutivity of symmetry for an inductive type *)
@@ -455,7 +455,7 @@ let build_l2r_rew_scheme dep env ind kind =
else
main_body))))))
in (c, UState.of_context_set ctx),
- Safe_typing.concat_private eff' eff
+ Evd.concat_side_effects eff' eff
(**********************************************************************)
(* Build the left-to-right rewriting lemma for hypotheses associated *)
@@ -708,7 +708,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,Safe_typing.empty_private_constants)
+ (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
(**********************************************************************)
(* Dependent rewrite from right-to-left in hypotheses *)
@@ -718,7 +718,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,Safe_typing.empty_private_constants)
+ (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
(**********************************************************************)
(* Dependent rewrite from left-to-right in hypotheses *)
@@ -728,7 +728,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,Safe_typing.empty_private_constants)
+ (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
(**********************************************************************)
(* Non-dependent rewrite from either left-to-right in conclusion or *)
@@ -742,7 +742,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), Safe_typing.empty_private_constants)
+ (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects)
(**********************************************************************)
(* Non-dependent rewrite from either right-to-left in conclusion or *)
@@ -752,7 +752,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, Safe_typing.empty_private_constants)
+ (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects)
(* End of rewriting schemes *)
@@ -836,4 +836,4 @@ 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,
- Safe_typing.empty_private_constants)
+ Evd.empty_side_effects)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 4749aebd96..c15fa146d4 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -27,7 +27,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 * Safe_typing.private_constants
+ constr Evd.in_evar_universe_context * Evd.side_effects
val build_r2l_forward_rew_scheme :
bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
val build_l2r_forward_rew_scheme :
@@ -39,7 +39,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 * Safe_typing.private_constants
+ constr Evd.in_evar_universe_context * Evd.side_effects
val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b9485b8823..539fe31416 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -31,9 +31,9 @@ open Pp
(* Registering schemes in the environment *)
type mutual_scheme_object_function =
- internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
type 'a scheme_kind = string
@@ -124,7 +124,7 @@ let define internal role id c poly univs =
let entry = {
const_entry_body =
Future.from_val ((c,Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
+ Evd.empty_side_effects);
const_entry_secctx = None;
const_entry_type = None;
const_entry_universes = univs;
@@ -145,10 +145,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let role = Entries.Schema (ind, kind) in
+ let role = Evd.Schema (ind, kind) in
let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
declare_scheme kind [|ind,const|];
- const, Safe_typing.concat_private neff eff
+ const, Evd.concat_side_effects neff eff
let define_individual_scheme kind mode names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
@@ -163,9 +163,9 @@ let define_mutual_scheme_base kind suff f mode names mind =
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let fold i effs id cl =
- let role = Entries.Schema ((mind, i), kind)in
+ let role = Evd.Schema ((mind, i), kind)in
let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
- (Safe_typing.concat_private neff effs, cst)
+ (Evd.concat_side_effects neff effs, cst)
in
let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
@@ -180,7 +180,7 @@ let define_mutual_scheme kind mode names mind =
let find_scheme_on_env_too kind ind =
let s = String.Map.find kind (Indmap.find ind !scheme_map) in
- s, Safe_typing.empty_private_constants
+ s, Evd.empty_side_effects
let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
try find_scheme_on_env_too kind ind
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 0eb4e47aeb..460b1f1b07 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -22,9 +22,9 @@ type individual
type 'a scheme_kind
type mutual_scheme_object_function =
- internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
(** Main functions to register a scheme builder *)
@@ -39,13 +39,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
val define_individual_scheme : individual scheme_kind ->
internal_flag (** internal *) ->
- Id.t option -> inductive -> Constant.t * Safe_typing.private_constants
+ Id.t option -> inductive -> Constant.t * Evd.side_effects
val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
- (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants
+ (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects
(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
val check_scheme : 'a scheme_kind -> inductive -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:15:37 +0000