Merge PR #12129: Add a `with_strategy` tactic

Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot

1 files changed, 0 insertions, 6 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3cb10364b5..049c3a0844 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -790,12 +790,6 @@ GRAMMAR EXTEND Gram
        { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
     ]
   ];
-  strategy_level:
-    [ [ IDENT "expand" -> { Conv_oracle.Expand }
-      | IDENT "opaque" -> { Conv_oracle.Opaque }
-      | n=integer -> { Conv_oracle.Level n }
-      | IDENT "transparent" -> { Conv_oracle.transparent } ] ]
-  ;
   instance_name:
     [ [ name = ident_decl; bl = binders ->
           { (CAst.map (fun id -> Name id) (fst name), snd name), bl }