Skip to content
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.

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

';' can be partially evaluated using Set Ltac Debug. #11

Open
palmskog opened this issue Aug 26, 2011 · 3 comments
Open

';' can be partially evaluated using Set Ltac Debug. #11

palmskog opened this issue Aug 26, 2011 · 3 comments
Labels
enhancement New feature or request major

Comments

@palmskog
Copy link
Member

Original report by Carst Tankink (Bitbucket: Carst, GitHub: Carst).


Investigate how useful this is when interfacing using Python (also with multiple goals).

@palmskog
Copy link
Member Author

Original comment by Jason Gross (Bitbucket: jasongross9, ).


Oooh, this seems like it'd be really cool.

@palmskog
Copy link
Member Author

Original comment by Carst Tankink (Bitbucket: Carst, GitHub: Carst).


Wow Issue-necro-ing!

Since then, there is a cooler option: prints of subgoals on arbitrary locations, combined with the PIDE library (for rebuilding a Proviola and/or giving feedback in an asynchronous interface): Enrico added the required code to Coq, the ';' tactical (and others) needs to be ported to support it. Bug the Coq devs and I'll see what I can do. ;)

@palmskog
Copy link
Member Author

Original comment by Jason Gross (Bitbucket: jasongross9, ).


Oops. I was reporting a bug, and looked at the issues new since the last time I was here.

Is there an appropriate feature request on the bug tracker to bug the Coq devs about? I don't quite understand what it would mean for the ';' tactical (or any others) to support this.

@palmskog palmskog added major enhancement New feature or request labels Jun 6, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request major
Projects
None yet
Development

No branches or pull requests

1 participant