diff options
Diffstat (limited to 'tactics/elimschemes.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 749e0d2b..8a6d93cf 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort ind = +let optimize_non_type_induction_scheme kind dep sort _ ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -51,8 +51,8 @@ let optimize_non_type_induction_scheme kind dep sort ind = let u = Univ.UContext.instance ctx in 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_env ~ctx:ectx env) (ind,u) dep sort in - (c, Evd.evar_universe_context sigma), Declareops.no_seff + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + (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 @@ -63,20 +63,20 @@ let build_induction_scheme_in_type dep sort ind = let u = Univ.UContext.instance ctx in 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_env ~ctx:ectx env) (ind,u) dep sort in + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in c, Evd.evar_universe_context sigma 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) |