New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix #518: "Proof using" mode corrupts "Proof with tac". #519

Merged

Matafou merged 1 commit into master from fix-518

Oct 16, 2020

Contributor

Matafou commented Oct 16, 2020

Fixing the auto insertion of Proof using in the case of a with annotation also present.


          Fix #518: "Proof using" mode corrupts "Proof with tac".

516c2c1

Matafou force-pushed the fix-518 branch from 4eeec0b to 516c2c1 Compare

October 16, 2020 15:15

Contributor Author

Matafou commented Oct 16, 2020

rebased.

Matafou merged commit eb6bba1 into master

erikmd mentioned this pull request

In Coq mode, "Proof using" mode corrupts "Proof with tac" #518

Closed

erikmd added the kind: fix label

erikmd deleted the fix-518 branch

November 26, 2021 00:32

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels