One can read the Coq documentation about discriminate tactic here.

Were is this tactic actually defined?

  • 1
    $\begingroup$ It's a builtin, it seems to be defined here at discr_tac. See also here. $\endgroup$
    – Couchy
    Jul 7, 2022 at 6:41
  • $\begingroup$ 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. $\endgroup$ Jul 8, 2022 at 12:26


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.