It is worth reading the entire roadmap. These are all comprehensible and important points. Coq seems to be a perpetual construction site. Ltac -> Ltac2 Prop

It is worth reading the entire roadmap. These are all comprehensible and important points. Coq seems to be a perpetual construction site. Ltac -> Ltac2 Prop -> Sprop On the other hand, my personal gimmicks a few years ago only touched on a tiny range of functions of the then Coq. Therefore, I assume that most Coq users see more stability than you would think.