Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"

1 files changed, 1 insertions, 11 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f15a64fc8..236db1dcc 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -69,20 +69,10 @@ let _ =
       optread  = (fun () -> !discriminate_introduction);
       optwrite = (:=) discriminate_introduction }
 
-let injection_pattern_l2r_order = ref true
-
 let use_injection_pattern_l2r_order = function
-  | None -> !injection_pattern_l2r_order
+  | None -> true
   | Some flags -> flags.injection_pattern_l2r_order
 
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
-      optkey   = ["Injection";"L2R";"Pattern";"Order"];
-      optread  = (fun () -> !injection_pattern_l2r_order) ;
-      optwrite = (fun b -> injection_pattern_l2r_order := b) }
-
 let injection_in_context = ref false
 
 let use_injection_in_context = function