Bring the newest features from main into coq-master

impermeable / coq-waterproof

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.

https://impermeable.github.io/

GNU Lesser General Public License v3.0

30 stars 9 forks source link

Bring the newest features from main into coq-master #76

Closed jim-portegies closed 1 month ago

jim-portegies commented 1 month ago

Create a devcontainer for the project
Check for binder names in the Take and Choose tactic
Refactor the ffi
Add a Waterproof version for the specialize tactic
Add explicit coercions for triple or statements
Add options to postpone proofs in It holds and We conclude that tactics
Disallow Qed as variable name in Induction and Obtain tactics
New form of expand definition: expand in all statements
Allow for blanks in the Choose and Specialize tactics

jim-portegies commented 1 month ago

I'll be merging this PR, rather than squashing and merging to restore the connections between the different branches.