Specification language
match
in
type_scope
function_scope
Arguments
Proofs
Proof using
Scheme
Derive
Inversion
dependent destruction
dependent induction
lra
lia
nra
nia
psatz
zify
nsatz
Type
L
Using Coq
Functional
coqrc
-vos
Appendix
Allow StrictProp
Asymmetric Patterns
Auto Template Polymorphism
Automatic Proposition Inductives
Boolean Equality Schemes
Bullet Behavior
Case Analysis Schemes
Contextual Implicit
Coqtop Exit On Error
Cumulativity Weak Constraints
Debug
Debug Auto
Debug Eauto
Debug Ssreflect
Debug SsrMatching
Debug Trivial
Decidable Equality Schemes
Default Goal Selector
Default Proof Mode
Default Proof Using
Default Timeout
Definitional UIP
Dependent Proposition Eliminators
Diffs
Dump Arith
Elimination Schemes
Extraction AutoInline
Extraction Conservative Types
Extraction File Comment
Extraction Flag
Extraction KeepSingleton
Extraction Optimize
Extraction Output Directory
Extraction SafeImplicits
Extraction TypeExpand
Fast Name Printing
Firstorder Depth
Firstorder Solver
Guard Checking
Hyps Limit
Implicit Arguments
Info Auto
Info Eauto
Info Level
Info Trivial
Intuition Negation Unfolding
Keep Equalities
Keep Proof Equalities
Kernel Term Sharing
Keyed Unification
Lia Cache
Loose Hint Behavior
Ltac Backtrace
Ltac Batch Debug
Ltac Debug
Ltac Profiling
Ltac2 Backtrace
Ltac2 In Ltac1 Profiling
Ltac2 Typed Notations
Mangle Names
Mangle Names Light
Mangle Names Prefix
Maximal Implicit Insertion
NativeCompute Profile Filename
NativeCompute Profiling
NativeCompute Timing
Nested Proofs Allowed
Nia Cache
Nonrecursive Elimination Schemes
Nra Cache
Parsing Explicit
Polymorphic Inductive Cumulativity
Positivity Checking
Primitive Projections
Printing All
Printing Allow Match Default Clause
Printing Coercion
Printing Coercions
Printing Compact Contexts
Printing Constructor
Printing Dependent Evars Line
Printing Depth
Printing Existential Instances
Printing Factorizable Match Patterns
Printing Float
Printing Goal Names
Printing Goal Tags
Printing If
Printing Implicit
Printing Implicit Defensive
Printing Let
Printing Match All Subterms
Printing Matching
Printing Notations
Printing Parentheses
Printing Primitive Projection Parameters
Printing Projections
Printing Raw Literals
Printing Record
Printing Records
Printing Relevance Marks
Printing Synth
Printing Unfocused
Printing Unfolded Projection As Match
Printing Universes
Printing Use Implicit Types
Printing Width
Printing Wildcard
Private Polymorphic Universes
Program Cases
Program Generalized Coercion
Program Mode
Regular Subst Tactic
Reversible Pattern Implicit
Rewriting Schemes
Search Blacklist
Search Output Name Only
Short Module Printing
Silent
Solve Unification Constraints
SsrHave NoTCResolution
SsrIdents
SsrOldRewriteGoalsOrder
SsrRewrite
Strict Implicit
Strict Universe Declaration
Strongly Strict Implicit
Structural Injection
Suggest Proof Using
Transparent Obligations
Typeclass Resolution For Conversion
Typeclasses Debug
Typeclasses Debug Verbosity
Typeclasses Default Mode
Typeclasses Dependency Order
Typeclasses Depth
Typeclasses Iterative Deepening
Typeclasses Limit Intros
Typeclasses Strict Resolution
Typeclasses Unique Instances
Typeclasses Unique Solutions
Uniform Inductive Parameters
Universe Checking
Universe Minimization ToSet
Universe Polymorphism
Warnings