Emilio Jesús Gallego Arias

@herbelin maybe not completely but it would certainly help.

@herbelin my impression is that proof modes as they stand now won't scale well for individual tactics, as you would need one proof mode for each particular tactic variation. One...

@mattam82 proof modes work, however I am concerned about scalability, in the sense that in the current state, you need to have a different proof mode for each tactic, which...

Yes you could. But we may really need "tactic modes" and "proof modes", in the sense that people may want to have different tactic language modes (LTAC / LTAC 2)...

@Zimmi48 yup, it would be good anyways to factor the ltac grammars a bit.

@herbelin the CEP looks pretty good to me, I'd say let's follow the plan. Worth mentioning too is the effort by Gaëtan ( cc @skyskimmer ) unifying both types using...

I like the idea for IMHO feels a bit overkill. Likely, using a PPX for lenses-style programming could be a better option.

> TBH I would look at stuff which comes before vernac/ first when reducing statefulness. Indeed, `engine` and `pretyping` seem like good candidates. > is an objective (so that we...

> And I guess that you don't like either that the induction name is n0 here: That's certainly a bit counter intuitive for folks used to functional programming. In typical...

> an horrible, but sensible, replacement is a path from the root to the term you want to point at. Randy Pollack had at some point a representation that was...