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/eqschemes.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/eqschemes.ml')
-rw-r--r-- | tactics/eqschemes.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0..8643fe10f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun _ ind -> + (fun ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun _ ind -> + (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,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,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,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,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,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,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,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 + (fun ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,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, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun _ ind -> + (fun ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) |