Changed: focus commands such as 1:{ and goal selection for query commands such as 1: Check do not need Classic (Ltac1) proof mode to function. In particular they function in Ltac2 mode (#18707, fixes #18351, by Gaëtan Gilbert).

Provide feedback

Saved searches