local context names

Stream: general

[Patrick Massot]

I have a silly tactic writing question. I know about local_context, which returns a tactic (list expr). But how do you get the names of the local hypotheses?

[Mario Carneiro]

each element in that list is a local_const

[Mario Carneiro]

so you can map local_pp_name on the list to get the names

[Patrick Massot]

Thanks!

[Patrick Massot]

I forgot what expr were...