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

Garbage-collect options in sanity.v #80

Merged
merged 1 commit into from
May 12, 2024
Merged

Garbage-collect options in sanity.v #80

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
17 changes: 1 addition & 16 deletions src/coqutil/sanity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,3 @@
Global Unset Universe Minimization ToSet.
Global Set Default Goal Selector "!".

(** Work around some counter-intuitive defaults. *)

(** [intuition] means [intuition auto with *]. This is very wrong and
fragile and slow. We make [intuition] mean [intuition auto]. *)
Tactic Notation "intuition" tactic3(tactic) := intuition tactic.
Tactic Notation "intuition" := intuition auto.

(** [firstorder] means [firstorder auto with *]. This is very wrong
and fragile and slow. We make [firstorder] mean [firstorder
auto]. *)
Global Set Firstorder Solver auto.

(** A version of [intuition] that allows you to see how the old
[intuition] tactic solves the proof. *)
Ltac debug_intuition := idtac "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; intuition debug auto with *.
Ltac Tauto.intuition_solver ::= auto with core.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If this is a new thing, you can do something like

Suggested change
Ltac Tauto.intuition_solver ::= auto with core.
Module Coq. Module ???. Module Tauto. Ltac intuition_solver := idtac. End Tauto. End ???. End Coq.
Ltac Coq.???.Tauto.intuition_solver ::= auto with core.

And rely on Coq refusing to shadow absolute names.