\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Programmable proof search

Tactics

Tactic auto nat_or_var? auto_using? hintbases?

auto_using::=using one_term+,hintbases::=with *|with ident+

Implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the assumption tactic, then it reduces the goal to an atomic one using intros and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated with the head symbol of the goal and tries to apply one of them. This process is recursively applied to the generated subgoals.

Within each hintbase, lower cost tactics are tried before higher-cost tactics. When multiple hintbases are specified, all hints in the first database are tried before any in the second database (and so forth) regardless of their cost (unlike eauto and typeclasses eauto).

nat_or_var: Specifies the maximum search depth. The default is 5.

using one_term+,

Uses lemmas one_term+, in addition to hints. If one_term is an inductive type, the collection of its constructors are added as hints.

Note that hints passed through the using clause are used in the same way as if they were passed through a hint database. Consequently, they use a weaker version of apply and auto using one_term may fail where apply one_term succeeds.

with *: Use all existing hint databases. Using this variant is highly discouraged in finished scripts since it is both slower and less robust than explicitly selecting the required databases.
with ident+: Use the hint databases ident+ in addition to the database core. Use the fake database nocore to omit core.

If no with clause is given, auto only uses the hypotheses of the current goal and the hints of the database named core.

auto generally either completely solves the goal or leaves it unchanged. Use solve [ auto ] if you want a failure when they don't solve the goal. auto will fail if fail or gfail are invoked directly or indirectly, in which case setting the Ltac Debug may help you debug the failure.

Warning

auto uses a weaker version of apply that is closer to simple apply so it is expected that sometimes auto will fail even if applying manually one of the hints would succeed.

Hint databases

Hints used by auto, eauto and other tactics are stored in hint databases. Each database maps head symbols to a list of hints. Use the Print Hint command to view a database.

Each hint has a cost and an optional pattern. Hints with lower cost are tried first. (Cost is not used to limit the scope of searches.) auto tries a hint when the conclusion of the current goal matches its pattern or when the hint has no pattern.

Creating hint databases

Use Create HintDb command to create hint databases. The new databases have the default setting Transparent for Constants, Projections and Variables. We recommend using Hint Constants, Hint Projections and Hint Variables immediately after Create HintDb to make these settings explicit.

Alternatively, adding a hint to an unknown database creates the latter implicitly, but this behavior is deprecated as of Rocq 9.2. Implicitly created databases have the Opaque setting for Constants, Projections and Variables.

The proof search tactics use unification to choose which tactics to try, for example whether the goal unifies with a theorem given by Hint Resolve.

Use Hint Opaque and Hint Transparent to control the opacity of individual items during this initial unification. These settings are distinct from the non-hint Opaque and Transparent settings. Hint opacity settings influence which hints the search tactics try, but in some cases they also affect how selected tactics are executed. (In particular, typeclasses eauto uses the equivalent of autoapply when applying Hint Resolve hints, which explicitly use the hint opacity settings. auto and eauto don't do this.)

Command Create HintDb ident discriminated?

If there is no hint database named ident, creates a new hint database with that name. Otherwise, does nothing.

All constants, variables and projections are set to default to unfoldable (use Hint Constants, Hint Projections and Hint Variables to change this). For better performance, we recommend setting each of these to Opaque and then using Hint Transparent for specific items when necessary.

By default, hint databases are undiscriminated. We recommend using discriminated because it generally performs better.

Deciding which hints to try

The proof search tactics decide which hints to try by first selecting hints whose pattern has the same head constant as the goal. Then the selected hints are tried as follows:

For hints other than Hint Extern: If the database is discriminated, only matching hints are tried. Hints match if all compared items that are opaque in both the goal and the pattern are identical. Marking definitions as Hint Opaque reduces the number of matches, but it may cause some proof searches that previously worked to fail.

Otherwise (if not discriminated), all hints will be tried. (Therefore, use discriminated databases whenever possible.)
For Extern hints: If the hint has a pattern, hints matching the goal will be tried. In this case, matching uses a form of syntactic unification), treating everything as hint opaque.

Otherwise (if there is no pattern), all hints will be tried. (Therefore, provide a pattern in Extern hints whenever possible.)

Command Create Rewrite HintDb ident: Like above, but creates a database for Hint Rewrite declarations instead.

Hint databases defined in the Rocq standard library

Several hint databases are defined in the Rocq standard library. The database contains the hints declared for it in the currently loaded modules (subject to locality attributes) as well as any added in the current module. Requiring additional modules (Require) may add more hints.

At Rocq startup, only the core database is nonempty and ready to be used immediately.

core:: This special database is automatically used by auto, except when pseudo-database nocore is given to auto. The core database contains only basic lemmas about negation, conjunction, and so on. Most of the hints in this database come from the Init and Logic directories.
arith:: all lemmas about Peano’s arithmetic proved in the directories Init and Arith.
zarith:: lemmas about binary signed integers from the directories theories/ZArith. The database also contains high-cost hints that call lia on equations and inequalities in nat or Z.
bool:: lemmas about booleans, mostly from directory theories/Bool.
datatypes:: lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory.
sets:: lemmas about sets and relations from the directories Sets and Relations.
typeclass_instances:: special database containing all typeclass instances declared in the environment, including those used for setoid_rewrite, from the Classes directory.
fset:: internal database for the implementation of the FSets library.
ordered_type:: lemmas about ordered types (as defined in the legacy OrderedType module), mainly used in the FSets and FMaps libraries.

You are advised not to put your own hints in the core database, but instead to use one or more databases specific to your development.

Creating Hints

The various Hint commands share these elements:

: ident+? specifies the hint database(s) to add to. (Deprecated since version 8.10: If no idents are given, the hint is added to the core database.)

Hints in hint databases are ordered, which is the order in which they're tried, as shown by the Print HintDb command. Hints with lower costs are tried first. Hints with the same cost are tried in reverse of their order of definition, i.e., last to first.

Rewrites with theorems such as forall n m, n+m=m+n or forall n m p, (n+m)+p=n+(m+p) (eg Hint Extern ... => rewrite ...) should be used only in Hint Immediate to prevent them from wastefully being applied .

Outside of sections, these commands support the local, export and global attributes. export is the default.

Inside sections, some commands only support the local attribute. These are Hint Immediate, Hint Resolve, Hint Constructors, Hint Unfold, Hint Extern and Hint Rewrite. local is the default for all hint commands inside sections.

local hints are never visible from other modules, even if they Import or Require the current module.

export hints are visible from other modules when they Import the current module, but not when they only Require it.

global hints are visible from other modules when they Require the current module (submodules of the current module are considered Required after their End).

Changed in version 8.18: The default value for hint locality outside sections is now export. It used to be global.

Deprecated since version 9.2: Implicitly creating a unknown database is now deprecated and will become an error.

The Hint commands are:

Command Hint Resolve qualidone_term+ hint_info? : ident+?

Command Hint Resolve -><- qualid+ natural? : ident+?

hint_info::=| natural? one_pattern?one_pattern::=one_term
The first form adds each qualid as a hint with the head symbol of the type of qualid to the specified hint databases (idents). If specified, natural is the cost of the hint; otherwise the cost of the hint is the number of subgoals generated by simple apply. The associated pattern is inferred from the conclusion of the type of qualid or, if specified, the given one_pattern.

If the inferred type of qualid does not start with a product, the command adds exact qualid to the hint list. If the type reduces to a type starting with a product, the command also adds simple apply qualid to the hints list. Note that tactics printed in debug output are similar to but not exactly the same as the ones executed by proof search. Unlike auto and eauto, typeclasses eauto uses a tactic equivalent to autoapply, which behaves somewhat differently from simple apply. Nonetheless, that tactic's debug output and the hint database misleadingly show simple apply.

If the inferred type of qualid contains a dependent quantification on a variable which occurs only in the premises of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is only used by eauto / typeclasses eauto, but not by auto. A typical hint that would only be used by eauto is a transitivity lemma.

-><-
The second form adds the left-to-right (->) or right-ot-left implication (<-) of a logical equivalence (<->) as a hint. If needed, it defines a projection for the specified direction, which the hint applies with a restricted version of apply. (For example, Hint Resolve -> and_comm defines and_comm_proj_l2r.)

one_term
Permits declaring a hint without declaring a new constant first. This is deprecated.

Warning Declaring arbitrary terms as hints is fragile and deprecated; it is recommended to declare a toplevel constant instead

one_pattern
Overrides the default pattern, which may occasionally be useful. For example, if a hint has the default pattern _ = _, you could limit the hint being tried only for bools with the pattern (@eq bool _ _).

Error qualid cannot be used as a hint

The head symbol of the type of qualid is a bound variable such that this tactic cannot be associated with a constant.

Command Hint Immediate qualidone_term+ : ident+?

For each specified qualid, adds the tactic simple apply qualid; solve [ trivial ] to the hint list associated with the head symbol of the type of qualid. The tactic fails if any of the subgoals generated by simple apply qualid are not solved immediately by trivial (which only tries tactics with cost 0). This hint is useful to allow controlled use of theorems such as n+m=m+n or (n+m)+p=n+(m+p) that otherwise could be applied repeatedly without limit. The cost of this hint (which never generates subgoals) is always 1, so it won't be used by trivial itself.

Command Hint Constructors qualid+ : ident+?

For each qualid that is an inductive type, adds all its constructors as hints of type Resolve. Then, when the conclusion of current goal has the form (qualid ...), auto will try to apply each constructor using exact.

Error qualid is not an inductive type

Command Hint Unfold qualid+ : ident+?

For each qualid, adds the tactic unfold qualid to the hint list that will only be used when the head constant of the goal is qualid. Its cost is 4.

Command Hint TransparentOpaque qualid+ : ident+?

Adds transparency hints to the database, making each qualid transparent or opaque during resolution. The proof search tactics use unification to determine whether to try most hints, for example checking if the goal unifies with the theorem used in a Hint Resolve hint. Currently the head constant is always treated as opaque (see example). See here for a description of how opaque and transparent affect which hints are tried. Note that transparency hints are independent of the non-hint Opaque and Transparent settings.

Example: Transparency with Multiple Hint Databases

To use different transparency settings for particular hints, put them in separate hint databases with distinct transparency settings and use typeclasses eauto. (This doesn't work for auto or eauto.):

Definition one := 1.
one is defined

Theorem thm : one = 1. reflexivity. Qed.
1 goal ============================ one = 1 No more goals.

Create HintDb db1.
Hint Opaque one : db1.
Hint Resolve thm | 1 : db1.
Create HintDb db2.
Goal 1 = 1.
1 goal ============================ 1 = 1

(* "one" is not unfolded because it's opaque in db1, where bar is *) Fail typeclasses eauto with db1 db2 nocore. (* fails with tc eauto *)
The command has indeed failed with message: Tactic failure: Proof search failed.

Succeed eauto with db1 db2 nocore. (* ignores the distinction *)
Succeed auto with db1 db2 nocore. (* ignores the distinction *)
Hint Resolve thm | 2 : db2.
(* "one" is unfolded because it's transparent (by default) in db2 *) Succeed typeclasses eauto with db1 db2 nocore.

Abort.

Example: Independence of Hint Opaque and Opaque

Definition one := 1.
one is defined

Opaque one. (* not relevant to hint selection *)
Theorem bar: 1=1. reflexivity. Qed.
1 goal ============================ 1 = 1 No more goals.

Create HintDb db. (* constants, etc. transparent by default *)
Hint Opaque one : db. (* except for "one" *)
Hint Resolve bar : db. (* hint is not tried if one is Hint Opaque *)
Set Typeclasses Debug Verbosity 1.
Goal one = 1.
1 goal ============================ one = 1

Fail typeclasses eauto with db nocore. (* fail: no match for (one = 1) *)
Debug: 1: looking for (one = 1) without backtracking Debug: 1: no match for (one = 1), 1 possibilities The command has indeed failed with message: Tactic failure: Proof search failed.

Hint Transparent one : db.
Succeed typeclasses eauto with db nocore. (* success: now bar is tried *)
Debug: 1: looking for (one = 1) without backtracking Debug: 1.1: exact bar on (one = 1), 0 subgoal(s)

Fail unfold one. (* fail: one is still Opaque *)
The command has indeed failed with message: one is opaque.

Abort.

Example: Head Constants are always opaque

Adding Hint Unfold Tru : db will make auto succeed. (If the goal was True = Tru, the head constant is eq and Tru will be unfolded.)

Definition Tru := True.
Tru is defined

Create HintDb db.
Hint Constants Transparent : db.
Hint Resolve I : db.
Print HintDb db. (*  For XXX -> indicates XXX is the head constant *)
Non-discriminated database Unfoldable variable definitions: all Unfoldable constant definitions: all Unfoldable projection definitions: all Cut: emp For any goal -> For True -> exact I (cost 0, pattern True, id 0)

Goal Tru.
1 goal ============================ Tru

Fail progress auto with db.
The command has indeed failed with message: Failed to progress.

Hint Unfold Tru : db. (* workaround *)
progress info_auto with db. (* works now! *)
(* info auto: *) unfold Tru (in db). exact I (in core). No more goals.

Abort.

Error Cannot coerce qualid to an evaluable reference.

Command Hint ConstantsProjectionsVariables TransparentOpaque : ident+?

Sets the default transparency for constants (from Definitions and Examples), projections (from Records and Structures) or variables (from Hypotheses and Variables) for the specified hint databases. Existing transparency settings for individual items (e.g., set with Hint Opaque) are dropped. Making items opaque can make proof search commands run faster (fewer unfoldings) but it can also prevent matching some hints. We recommend setting each of these to Opaque and then using Hint Transparent for specific items as needed. We advise using this command just after a Create HintDb command.

Command Hint Extern natural one_pattern? => generic_tactic : ident+?

Extends auto with tactics other than apply and unfold. natural is the cost, one_pattern is the pattern to match and ltac_expr is the action to apply.

We recommend providing a pattern whenever possible. Hints with patterns are tried only if the pattern matches without unfolding transparent constants (i.e., a syntactic match). Hints without patterns are always tried.

Usage tip: tactics that can succeed even if they don't change the context, such as most of the conversion tactics, should be prefaced with progress to avoid needless repetition of the tactic.

Usage tip: Use a Hint Extern with no pattern to do pattern matching on hypotheses using match goal with inside the tactic.

Example

Hint Extern 4 (~(_ = _)) => discriminate : core.

Now, when the head of the goal is an inequality, auto will try discriminate if it does not manage to solve the goal with hints with a cost less than 4.

One can even use some sub-patterns of the pattern in the tactic script. A sub-pattern is a question mark followed by an identifier, like ?X1 or ?X2. Here is an example:

Example

Require Import ListDef.
Create HintDb eqdec.
Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) =>   generalize X1, X2; decide equality : eqdec.
Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
1 goal ============================ forall a b : list (nat * nat), {a = b} + {a <> b}

info_auto with eqdec.
(* info auto: *) intro. intro. (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). No more goals.

Command Hint Cut [ hints_regexp ] : ident+?

hints_regexp::=qualid+(hint or instance identifier)|_(any hint)|hints_regexp | hints_regexp(disjunction)|hints_regexp hints_regexp(sequence)|hints_regexp *(Kleene star)|emp(empty)|eps(epsilon)|( hints_regexp )
Adds another clause to the cut regular expression in the specfied hint databases. Hint Cut hints_regexp sets the cut expression to c | hints_regexp. The initial cut expression is emp.

Typeclass proof search and the typeclasses eauto tactic (but not auto or eauto) use the cut expression to conditionally prevent using some hints based on the path of hints that have been successfully applied. The path is an ordered list of hint identifiers. When the path plus the identifier of a candidate hint matches the cut expression, the hint is not applied. (It is nothing like a cut in Prolog.)

The hint identifier is the qualid that appears in the various Hint commands (e.g. as in Hint Resolve plus_O_n.), with the following exceptions:

Hint Externs do not have associated identifiers

For Hint Constructors, which creates multiple hints, the identifiers are the names of the constructors.

For Hint Resolve -><- theorem, the name is theorem_proj_l2r or theorem_proj_r2l depending on the direction of the arrow.

The output of Print HintDb shows the cut expression.

Warning

The regexp matches the entire path. Most hints will start with a leading ( _* ) to match the tail of the path. (Note that (_*) misparses since *) would end a comment.)

Warning

There is no operator precedence during parsing, one can check with Print HintDb to verify the current cut expression.

Command Hint Mode qualid +!-+ : ident+?

Sets an optional mode of resolution for the identifier qualid. When proof search has a goal that ends in an application of qualid to arguments arg ... arg, the mode tells if the hints associated with qualid can be applied or not, depending on a criterion on the arguments. A mode specification is a list of +, ! or - items that specify if an argument of the identifier is to be treated as an input (+), if its head only is an input (!) or an output (-) of the identifier. Mode - matches any term, mode + matches a term if and only if it does not contain existential variables, while mode ! matches a term if and only if the head of the term is not an existential variable. The head of a term is understood here as the applicative head, recursively, ignoring casts. For a mode declaration to match a list of arguments, each argument should match its corresponding mode.

Only typeclasses eauto uses these hints. Hint Mode is especially useful for typeclasses, when one does not want to support default instances and wants to avoid ambiguity in general. Setting a parameter of a class as an input forces proof search to be driven by that index of the class, with ! allowing existentials to appear in the index but not at its head.

Note

Multiple modes can be declared for a single identifier. In that case only one mode needs to match the arguments for the hints to be applied.

If you want to add hints such as Hint Transparent, Hint Cut, or Hint Mode, for typeclass resolution, do not forget to put them in the typeclass_instances hint database.

Warning This hint is not local but depends on a section variable. It will disappear when the section is closed.

A hint with a non-local attribute was added inside a section, but it refers to a local variable that will go out of scope when closing the section. As a result the hint will not survive either.

Example: Logic programming with addition on natural numbers

This example illustrates the use of modes to control how resolutions can be triggered during proof search.

Parameter plus : nat -> nat -> nat -> Prop.
plus is declared

Create HintDb plus.
Hint Mode plus ! - - : plus.
Hint Mode plus - ! - : plus.

Axiom plus0l : forall m : nat, plus 0 m m.
plus0l is declared

Axiom plus0r : forall n : nat, plus n 0 n.
plus0r is declared

Axiom plusSl : forall n m r : nat, plus n m r -> plus (S n) m (S r).
plusSl is declared

Axiom plusSr : forall n m r : nat, plus n m r -> plus m (S m) (S r).
plusSr is declared

Hint Resolve plus0l plus0r plusSl plusSr : plus.
The hint plusSr will only be used by eauto, because applying plusSr would leave variable n as unresolved existential variable.

The previous commands define the addition predicate and set its mode so it can resolve goals if and only if one of the first two arguments is headed by a constructor or constant. The last argument of the predicate will be the inferred result.

Goal exists x y, plus x y 12.
1 goal ============================ exists x y : nat, plus x y 12

Proof. eexists ?[x], ?[y].
1 focused goal (shelved: 2) ============================ plus ?x ?y 12

   Fail typeclasses eauto with plus.
The command has indeed failed with message: Tactic failure: Proof search failed.

   instantiate (y := 1).
1 focused goal (shelved: 1) ============================ plus ?x 1 12

   typeclasses eauto with plus.
No more goals.

Defined.

In the proof script, the first call to typeclasses eauto fails as the two arguments are headed by an existential variable, while when we instantiate the second argument with 1, typeclass resolution succeeds as the second declared mode is matched, and instantiates x with 11.

Command Hint Rewrite -><-? one_term+ using generic_tactic? : ident+?

using generic_tactic?: If specified, generic_tactic is applied to the generated subgoals, except for the main subgoal.
-><-: Arrows specify the orientation; left to right (->) or right to left (<-). If no arrow is given, the default orientation is left to right (->).

Adds the terms one_term+ (their types must be equalities) to the rewriting bases ident*. Note that the rewriting bases are distinct from the auto hint bases and that auto does not take them into account.

Command Print Rewrite HintDb ident: This command displays all rewrite hints contained in ident.

Command Remove Hints qualid+ : ident+?: Removes the hints associated with the qualid+ in databases ident+. Hints removals within sections are local to the section. Note: hints created with Hint Extern currently can't be removed because they aren't associated with names. The best workaround for this is to make the hints non-global and carefully select which modules you import.

Command Print Hint *reference?

*: Display all declared hints.
reference: Display all hints associated with the head symbol reference.

Displays tactics from the hints list. The default is to show hints that apply to the conclusion of the current goal. The other forms with * and reference can be used even if no proof is open.

Each hint has a cost that is a nonnegative integer and an optional pattern. The hints with lower cost are tried first.

Command Print HintDb ident: This command displays all hints from database ident. Hints are grouped by the head constants of their patterns ("For ... ->"). The groups are shown ordered alphabetically on the last component of the head constant name. Within each group, hints are shown in the order in which they will be tried (first to last). Note that hints with the same cost are tried in reverse of the order they're defined in, i.e., last defined is used first. Mode of resolution symbols, +!-+, when defined with Hint Mode, appear after the head constant.

Setting implicit automation tactics

Command Proof with generic_tactic using section_var_expr?: Starts a proof in which generic_tactic is applied to the active goals after each tactic that ends with ... instead of the usual single period. "tactic..." is equivalent to "tactic; generic_tactic.".

See also

Proof in Entering and exiting proof mode.