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.

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

Request: Version of Guarded for "please make sure I'm not going to get an error / anomaly on Qed" #9911

Closed
JasonGross opened this issue Apr 5, 2019 · 1 comment · Fixed by #17467
Closed

Request: Version of Guarded for "please make sure I'm not going to get an error / anomaly on Qed" #9911

JasonGross opened this issue Apr 5, 2019 · 1 comment · Fixed by #17467
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: feature New user-facing feature request or implementation.
Milestone
8.18+rc1

Comments

@JasonGross
Copy link
Member

I would like a version of Guarded that works to catch things like:

Goal False /\ True.
  split.
  exact_no_check I.
  Guarded. (* or `FakeQed` or whatever *)

Effectively, I want it to be roughly equivalent to me doing

Axiom admit : forall {T}, T.

and then doing

Unshelve.
all: exact admit.
Qed.

except without having to redo the whole proof if it succeeds and I want to backtrack.
@JasonGross JasonGross added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: feature New user-facing feature request or implementation. labels Apr 5, 2019
@JasonGross
Copy link
Member Author

I want this after getting bitten by anomalies and errors that only show up on Qed

@andres-erbsen andres-erbsen mentioned this issue Apr 9, 2019
Closed
@SkySkimmer SkySkimmer mentioned this issue May 26, 2023
Merged
@coqbot-app coqbot-app bot added this to the 8.18+rc1 milestone Jun 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: feature New user-facing feature request or implementation.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging a pull request may close this issue.

Validate Proof command: runs typing.ml on the current proof SkySkimmer/coq
1 participant
@JasonGross