aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eqschemes.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 073d66e4aa..3fdd97616f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -686,11 +686,6 @@ let build_r2l_rew_scheme dep env ind k =
let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in
c, Evd.evar_universe_context sigma
-let build_l2r_rew_scheme = build_l2r_rew_scheme
-let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme
-let build_r2l_rew_scheme = build_r2l_rew_scheme
-let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
-
(**********************************************************************)
(* Register the rewriting schemes *)
(**********************************************************************)