tactic.customEliminators

Default value: true

enable using custom eliminators in the 'induction' and 'cases' tactics defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes

tactic.skipAssignedInstances

Default value: true

in the rw and simp tactics, if an instance implicit argument is assigned, do not try to synthesize instance.

tactic.simp.trace

Default value: false

When tracing is enabled, calls to simp or dsimp will print an equivalent simp only call.