where:NTacStatus.tactic_pattern -> NTacStatus.tactic
val letin_tac:
where:NTacStatus.tactic_pattern ->
what: NTacStatus.tactic_term ->
string -> NTacStatus.tactic
where:NTacStatus.tactic_pattern -> NTacStatus.tactic
val letin_tac:
where:NTacStatus.tactic_pattern ->
what: NTacStatus.tactic_term ->
string -> NTacStatus.tactic