# Where is the discriminate tactic defined in Coq?

One can read the Coq documentation about discriminate tactic here.

Were is this tactic actually defined?

• It's a builtin, it seems to be defined here at discr_tac. See also here.
– Couchy
Jul 7, 2022 at 6:41
• Thank you! I'm interested in developing a bit more precise understanding of how tactics transform terms in the proof environment. I've seen some LTAC and I think it would be interesting to see how tactics operate under the hood. Jul 8, 2022 at 12:26