Adapt the various "Let" ended with Qed #82
Conversation
In sections: use #[clearbody] and Defined instead At toplevel: use Local Lemma instead
herbelin
changed the title
|
Thnaks! As you've seen we currently have coq/coq#17576 which IMHO would be the perfect solution to all that mess, at least the way it is used in the mathcomp world. |
Is there a summary of the situation somewhere (problems and solutions)? I'm lost in all the discussions. |
|
Maybe the last two messages: coq/coq#17576 (comment) |
I was thinking at a summary of the issues with Let (what to do with Admitted, #16893; effect of Qed on context initialization of other theorems, ...). In particular, I wonder if we would not save the burden of abstract and of having to address the warning by keeping Let as it is but letting its opacity have an impact (by uniformity of behavior) on other declarations of the context. Would there be a known problem at doing so? |
In sections: use #[clearbody] and Defined instead (see coq/coq#17205)
At toplevel: use Local Lemma instead
Assuming that this was the intended correction.