sig
  type lemma = Definitions.dlemma Tactical.named
  val named : Definitions.dlemma -> TacLemma.lemma
  val find : string -> TacLemma.lemma option
  val search : TacLemma.lemma option Tactical.field
  val tactical : Tactical.tactical
  val strategy :
    ?priority:float ->
    ?at:Tactical.selection ->
    string -> Tactical.selection list -> Strategy.strategy
end