diff options
author | 2015-10-29 13:04:22 +0100 | |
---|---|---|
committer | 2015-10-29 13:11:38 +0100 | |
commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /tactics/eqschemes.ml | |
parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'tactics/eqschemes.ml')
-rw-r--r-- | tactics/eqschemes.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0..b2603315d 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) |