Jason Gross

Ah, sorry, I did not realize that this PR was draft, and only noticed being tagged.

> "Control Structures" (repeat, if, ...) and "Handling tactic failures" These seem like good categories. Could you put a list of the existing headings together here, and I'll see if...

A first stab at categories: #### I think the following are proper semantics: Types of values Syntactic values Tactics in terms Substitution Local definitions: let Function construction and application ####...

The problem with `match` as a switch statement as control flow is that it emphasizes the wrong thing IMO. There's a way in which the interesting thing about a switch...

Does anything change if you use `@Rle_trans` instead of `Rle_trans`? If you're looking to apply something in a hypothesis, I'd suggest starting by looking at an iff lemma. (This will...

And I'm guessing you want ``` apply Rle_trans with (x * x ^ n) (y * y ^ n) (y * x ^n) in H. ``` (I swapped the last...

> None of the following work. IIUC they should match the non-dependent hypotheses of Rle_trans. You are using types where you should be using terms. Replace `apply Rle_trans with (n...

In `apply Rle_trans with (1 := x * x ^ n

@jfehrle I think most of it is fine, but saying that hypotheses and unproven goals have no proof terms is technically wrong. They have no *closed* proof term, but the...

Are you missing the following (from this and/or the deprecation PR)? https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/declare.ml#L974-L977 https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/classes.ml#L46-L50 and maybe these too (but can these even be changed by attributes?) https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/comAssumption.ml#L231-L234 https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/comAssumption.ml#L60 https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/classes.ml#L275-L282 https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/classes.ml#L618-L623 https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/plugins/ltac/comRewrite.ml#L79