Vernacular Options Index

  • Printing Implicit, 2.7.14
  • Printing Implicit Defensive, 2.7.14
  • Printing Matching, 2.2.4
  • Printing Notations, 12.1.9
  • Printing Primitive Projection Compatibility, 2.1.1
  • Printing Primitive Projection Parameters, 2.1.1
  • Printing Projections, 2.1
  • Printing Records, 2.1
  • Printing Synth, 2.2.4
  • Printing Unfocused, 6.9.15, 6.9.16, 6.9.17
  • Printing Universes, 2.10
  • Printing Width, 6.9.6, 6.9.7, 6.9.8
  • Printing Wildcard, 2.2.4
  • Program Generalized Coercion, 24.1
  • Program Cases, 24.1

  • Refine Instance Mode, 20.6.20
  • Refolding Reduction, 8.7.4
  • Regular Subst Tactic, 8.6.3
  • Reversible Pattern Implicit, 2.7.9

  • Search Output Name Only, 6.9.4, 6.9.5
  • Shrink Abstract, 9.2
  • Shrink Obligations, 24.2
  • Silent, 6.9.1, 6.9.2
  • Strict Implicit, 2.7.7
  • Strict Universe Declaration, 29.7.4
  • Strongly Strict Implicit, 2.7.7
  • Structural Injection, 8.5.7
  • Suggest Proof Using, 7.1.5

  • Tactic Compat Context, 9.2
  • Transparent Obligations, 24.2
  • Typeclasses Debug, 20.6.19
  • Typeclasses Debug Verbosity, 20.6.19
  • Typeclasses Dependency Order, 20.6.8
  • Typeclasses Filtered Unification, 20.6.9
  • Typeclasses Legacy Resolution, 20.6.10
  • Typeclasses Limit Intros, 20.6.12
  • Typeclasses Modulo Eta, 20.6.11
  • Typeclasses Resolution After Apply, 20.6.13
  • Typeclasses Resolution For Conversion, 20.6.14
  • Typeclasses Strict Resolution, 20.6.15
  • Typeclasses Unique Instances, 20.6.17
  • Typeclasses Unique Solutions, 20.6.16

  • Universal Lemma Under Conjunction, 8.2.4
  • Universe Minimization ToSet, 29.6
  • Universe Polymorphism, 29.2

  • Warnings, 6.9.3