Title: Where is the discriminate tactic defined in Coq?
Tags: coq;beginner;reference-request;tactic
Question: One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
Comment: It's a builtin, it seems to be defined [here](https://github.com/coq/coq/blob/master/tactics/equality.ml) at `discr_tac`. See also [here](https://github.com/coq/coq/blob/master/plugins/ltac/extratactics.mlg).

Comment: 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.



{'source': 'StackExchangeDataset', 'subset': 'proofassistants.stackexchange.com', 'metadata': {'AnswerCount': 0, 'CommentCount': 2, 'ContentLicense': 'CC BY-SA 4.0', 'CreationDate': '2022:00:07/07/22', 'FavoriteCount': None, 'PostTypeId': 1, 'Tags': '<coq><beginner><reference-request><tactic>', 'Title': 'Where is the discriminate tactic defined in Coq?', 'ViewCount': 61, 'id': 1574, 'user_AboutMe': None, 'user_AccountId': 25745862.0, 'user_DisplayName': 'Jacob woolcutt', 'user_Reputation': 31.0, 'user_Views': 0.0, 'user_id': 1477.0}}