The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
Adapt to https://github.com/coq/coq/pull/19530
This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future).
Merging this is not required for the upstream PR, you can do whatever you want with it.
Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future). Merging this is not required for the upstream PR, you can do whatever you want with it.