diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:31:00 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:35:53 +0200 |
commit | 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b (patch) | |
tree | ffcf6a36e224f1a41996f7ede84d773753254209 /tactics/elimschemes.ml | |
parent | 707bfd5719b76d131152a258d49740165fbafe03 (diff) |
Reverting 16 last commits, committed mistakenly using the wrong push command.
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
Diffstat (limited to 'tactics/elimschemes.ml')
-rw-r--r-- | tactics/elimschemes.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index dbaa60d61..749e0d2b5 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 @@ -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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) 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, Declareops.no_seff) |